lean_workbook_plus_65514

Proved

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

Prove the following inequality:\n $\frac{|a|}{1+|a|}+\frac{|b|}{1+|b|}\geq \frac{|a+b|}{1+|a+b|}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_65514 : ∀ a b : ℝ, (|a| / (1 + |a|) + |b| / (1 + |b|) : ℝ) ≥ |a + b| / (1 + |a + b|)   :=  by sorry

Source