abs_sub_lt_one_of_floor_eq_floor — Mathlib

English

If ⌊a⌋ = ⌊b⌋, then |a − b| < 1.

Русский

Если ⌊a⌋ = ⌊b⌋, то |a − b| < 1.

LaTeX

$$$$\text{If } \lfloor a \rfloor = \lfloor b \rfloor,\ \lvert a - b \rvert < 1.$$$$

Lean4

theorem abs_sub_lt_one_of_floor_eq_floor {R : Type*} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] [FloorRing R]
    {a b : R} (h : ⌊a⌋ = ⌊b⌋) : |a - b| < 1 :=
  by
  have : a < ⌊a⌋ + 1 := lt_floor_add_one a
  have : b < ⌊b⌋ + 1 := lt_floor_add_one b
  have : (⌊a⌋ : R) = ⌊b⌋ := Int.cast_inj.2 h
  have : (⌊a⌋ : R) ≤ a := floor_le a
  have : (⌊b⌋ : R) ≤ b := floor_le b
  exact abs_sub_lt_iff.2 ⟨by linarith, by linarith⟩

Похожие утверждения