lean_workbook_plus_78681

Proved

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

For RHS, we have $\\frac{1}{1+x} +\\frac{1}{1+y} \\leq \\frac{1}{1+0} +\\frac{1}{1+x+y}$ for all $0\\leq x,y \\leq 1$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_78681 : ∀ x y : ℝ, 0 ≤ x ∧ 0 ≤ y ∧ x ≤ 1 ∧ y ≤ 1 → 1 / (1 + x) + 1 / (1 + y) ≤ 1 / (1 + 0) + 1 / (1 + x + y)   :=  by sorry

Source

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

View graph