lean_workbook_plus_3871

Proved

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

Prove that for non-negative numbers x and y the following inequalities holds \n $\frac{x+y}{x+y+1}\le \frac{x}{x+1}+\frac{y}{y+1}\le \frac{2(x+y)}{x+y+2}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_3871 (x y : ℝ) (hx : 0 ≤ x) (hy : 0 ≤ y) : (x + y) / (x + y + 1) ≤ x / (x + 1) + y / (y + 1) ∧ x / (x + 1) + y / (y + 1) ≤ (2 * (x + y)) / (x + y + 2)   :=  by sorry

Source

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

View graph