lean_workbook_plus_2076

Proved

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

Let $a,b\in [1,2]$ . Prove that \n

\frac{4}{3}\leq\frac{a+1}{b+2}+\frac{b+1}{a+2} \leq \frac{3}{2}

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_2076 (a b : ℝ) (hab: a ∈ Set.Icc 1 2 ∧ b ∈ Set.Icc 1 2): 4/3 ≤ (a+1)/(b+2) + (b+1)/(a+2) ∧ (a+1)/(b+2) + (b+1)/(a+2) ≤ 3/2   :=  by sorry

Source

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

View graph