lean_workbook_plus_24359

Proved

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

If $a \in \mathbb R+$ , prove that there is a perfect square in $[a^2,(a+1)^2]$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_24359 (a : ℝ) (ha : 0 < a) : ∃ x, x^2 ∈ Set.Icc (a^2) ((a + 1)^2)   :=  by sorry

Source