lean_workbook_plus_50601

Proved

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

Prove that $\frac{\left | a-b \right |}{1+\left | a-b \right |}\leq \frac{\left | a \right |}{1+\left | a \right |}+\frac{\left | b \right |}{1+\left | b \right |}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_50601 (a b : ℝ) :  |a - b| / (1 + |a - b|) ≤ |a| / (1 + |a|) + |b| / (1 + |b|)   :=  by sorry

Source

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

View graph