lean_workbook_plus_34508

Proved

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

Verify it for $n=2$ ; indeed we have $\sqrt{\frac{1}{5}} < \frac{1}{2} < \sqrt{\frac{1}{3}}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_34508 : ∀ n : ℕ, n = 2 → Real.sqrt (1 / 5) < 1 / 2 ∧ 1 / 2 < Real.sqrt (1 / 3)   :=  by sorry

Source