lean_workbook_plus_65861
ProvedDoes imply ?
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_65861 (a b : ℝ) (h : ⌊a⌋ = b) : a - 1 ≤ b ∧ b ≤ a := by sorry
Source
Does imply ?
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_65861 (a b : ℝ) (h : ⌊a⌋ = b) : a - 1 ≤ b ∧ b ≤ a := by sorry