lean_workbook_plus_15478
ProvedAnd for we have and
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_15478 : ∀ x : ℝ, 1 > x ∧ x > 0 → ↑⌊x⌋ = 0 ∧ 0 ≤ √x ∧ √x < 1 := by sorry
Source
And for we have and
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_15478 : ∀ x : ℝ, 1 > x ∧ x > 0 → ↑⌊x⌋ = 0 ∧ 0 ≤ √x ∧ √x < 1 := by sorry