lean_workbook_plus_54024
ProvedSince
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_54024 (x : ℝ) : x - 1 < ⌊x⌋ ∧ ⌊x⌋ ≤ x := by sorry
Source
Since
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_54024 (x : ℝ) : x - 1 < ⌊x⌋ ∧ ⌊x⌋ ≤ x := by sorry