Prove2Me

lean_workbook_plus_3627

Proved

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

Prove that a,b∈R \quad a,b\in\mathbb{R}\n\n∣a+b∣1+∣a+b∣≤∣a∣1+∣a∣+∣b∣1+∣b∣ \frac{\lvert a+b\rvert}{1+\lvert a+b\rvert}\le\frac{\lvert a\rvert}{1+\lvert a\rvert}+\frac{\lvert b\rvert}{1+\lvert b\rvert}

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_3627 (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