Prove2Me

lean_workbook_plus_14391

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

By the triangle inequality: ∣xy−1∣=∣(x−1)+(y−1)+(x−1)(y−1)∣≤∣x−1∣+∣y−1∣+∣(x−1)(y−1)∣|xy-1|=|(x-1)+(y-1)+(x-1)(y-1)|\leq |x-1|+|y-1|+|(x-1)(y-1)| \nSo 1+∣xy−1∣≤1+∣x−1∣+∣y−1∣+∣x−1∣∣y−1∣=(1+∣x−1∣)(1+∣y−1∣)1+|xy-1|\leq 1+|x-1|+|y-1|+|x-1||y-1|=(1+|x-1|)(1+|y-1|)

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_14391  (x y : ℝ) :
  1 + |x * y - 1| ≤ (1 + |x - 1|) * (1 + |y - 1|)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph