lean_workbook_plus_82228

Proved

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

proofwiki

So the following inequality is true $\frac{1}{1+|a|}+\frac{1}{1+|b|}\leq 1+ \frac{1}{(1+|a|)(1+|b|)}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_82228 : ∀ a b : ℝ, 1 / (1 + |a|) + 1 / (1 + |b|) ≤ 1 + 1 / ((1 + |a|) * (1 + |b|))   :=  by sorry

Source