lean_workbook_plus_78853
Provedwhere (so it can be bound by 1/2)
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_78853 (x : ℝ) : |x - ⌊x⌋ - 1 / 2| ≤ 1 / 2 := by sorry
Source
where (so it can be bound by 1/2)
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_78853 (x : ℝ) : |x - ⌊x⌋ - 1 / 2| ≤ 1 / 2 := by sorry