Sum_of_Floor_and_Floor_of_Negative
Provedfloor-functionproofwiki
If x is not an integer, then ⌊x⌋ + ⌊-x⌋ = -1.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Sum_of_Floor_and_Floor_of_Negative (x : ℝ) (hx : ¬∃ n : ℤ, x = ↑n) : ⌊x⌋ + ⌊-x⌋ = -1 := by sorry
Source