lean_workbook_plus_40889
Provedprove:
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_40889 (x : ℝ) : x - 1 ≤ ⌊x⌋ ∧ ⌊x⌋ ≤ x := by sorry
Source
prove:
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_40889 (x : ℝ) : x - 1 ≤ ⌊x⌋ ∧ ⌊x⌋ ≤ x := by sorry