English
For real numbers a and b, fract(a) = b if and only if 0 ≤ b < 1 and a − b is an integer.
Русский
Пусть a и b вещественные; fract(a) = b тогда и только тогда, когда 0 ≤ b < 1 и a − b целое число.
LaTeX
$$$\\\\operatorname{fract}(a) = b \\\\iff 0 \\\\le b \\\\land b < 1 \\\\land \\\\exists z: \\\\mathbb{Z}, a - b = z$$$
Lean4
theorem fract_eq_iff {a b : R} : fract a = b ↔ 0 ≤ b ∧ b < 1 ∧ ∃ z : ℤ, a - b = z :=
⟨fun h => by
rw [← h]
exact ⟨fract_nonneg _, fract_lt_one _, ⟨⌊a⌋, sub_sub_cancel _ _⟩⟩,
by
rintro ⟨h₀, h₁, z, hz⟩
rw [← self_sub_floor, eq_comm, eq_sub_iff_add_eq, add_comm, ← eq_sub_iff_add_eq, hz, Int.cast_inj, floor_eq_iff, ←
hz]
constructor <;> simpa [sub_eq_add_neg, add_assoc]⟩
