lean_workbook_plus_75536

Proved

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

Does the following inequality hold for all real numbers $\sqrt{1-u} \leq |1- \frac{1}{2}u|$ ???

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_75536 (u : ℝ) : Real.sqrt (1 - u) ≤ |1 - 1 / 2 * u|   :=  by sorry

Source