fract_eq_fract — Mathlib

English

For all a,b in R, fract(a) = fract(b) if and only if a − b is an integer.

Русский

Для любых a, b в R, fract(a) = fract(b) тогда и только тогда, когда a − b — целое число.

LaTeX

$$$\\\\operatorname{fract}(a) = \\\\operatorname{fract}(b) \\\\iff \\\\exists z \\\\: \\\\mathbb{Z}, a - b = z$$$

Lean4

theorem fract_eq_fract {a b : R} : fract a = fract b ↔ ∃ z : ℤ, a - b = z :=
  ⟨fun h => ⟨⌊a⌋ - ⌊b⌋, by unfold fract at h; rw [Int.cast_sub, sub_eq_sub_iff_sub_eq_sub.1 h]⟩,
    by
    rintro ⟨z, hz⟩
    refine fract_eq_iff.2 ⟨fract_nonneg _, fract_lt_one _, z + ⌊b⌋, ?_⟩
    rw [eq_add_of_sub_eq hz, add_comm, Int.cast_add]
    exact add_sub_sub_cancel _ _ _⟩

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