lean_workbook_plus_47636
Proved[x] is meant as the biggest integer smaller than . So
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_47636 (x : ℝ) : ↑⌊x⌋ ≤ x ∧ x < ↑⌊x⌋ + 1 := by sorry
Source
[x] is meant as the biggest integer smaller than . So
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_47636 (x : ℝ) : ↑⌊x⌋ ≤ x ∧ x < ↑⌊x⌋ + 1 := by sorry