lean_workbook_plus_78624

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|}} \\le \\frac{{\\left| a \\right|}}{{1 + \\left| a \\right|}} + \\frac{{\\left| b \\right|}}{{1 + \\left| b \\right|}}\\quad ,\\forall a,b \\in R$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_78624 (a b : ℝ) : (abs (a + b) : ℝ) / (1 + abs (a + b)) ≤ abs a / (1 + abs a) + abs b / (1 + abs b)   :=  by sorry

Source

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

View graph