lean_workbook_plus_78123

Proved

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

You can use this fact: $|x-f(y)|=|(x-f(x))+(f(x)-f(y))|\leq |x-f(x)|+|f(x)-f(y)|$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_78123 (f : ℝ → ℝ) (x y : ℝ) :
  |x - f y| = |(x - f x) + (f x - f y)| ∧
  |x - f y| ≤ |x - f x| + |f x - f y|   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph