lean_workbook_plus_43107

Proved

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

Given $1\le a, b\le3$ and $a+b=4$ , prove that $|\sqrt{a}-\sqrt{b}| \le \sqrt{3}-1$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_43107 (a b : ℝ) (h₁ : 1 ≤ a ∧ a ≤ 3) (h₂ : 1 ≤ b ∧ b ≤ 3) (h₃ : a + b = 4) : |Real.sqrt a - Real.sqrt b| ≤ Real.sqrt 3 - 1   :=  by sorry

Source

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

View graph