lean_workbook_plus_15300

Proved

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

$x>0\Longrightarrow \sqrt x\le \frac{1+x}{2}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_15300 (x : ℝ) (hx : 0 < x) : Real.sqrt x ≤ (1 + x) / 2   :=  by sorry

Source