lean_workbook_plus_719

Proved

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

If $x,y \in R$ , then show that: \n $\frac {|x+y|} {1+|x+y|} \le \frac {|x|} {1+|x|}+ \frac {|y|} {1+|y|}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_719 (x y : ℝ) : (abs (x + y) / (1 + abs (x + y))) ≤ abs x / (1 + abs x) + abs y / (1 + abs y)   :=  by sorry

Source