lean_workbook_plus_58886

Proved

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

Explain why taking the square root on both sides of an inequality, assuming $a > b > 0$ , is a valid step to show that $\sqrt{a} > \sqrt{b}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_58886 (a b : ℝ) (h₁ : a > b) (h₂ : b > 0) : Real.sqrt a > Real.sqrt b   :=  by sorry

Source