English
For any x ∈ α and z ∈ ℤ, |x − round x| ≤ |x − z|.
Русский
Для любых x и z целых выполняется не превосходит расстояние до любого z: |x − round x| ≤ |x − z|.
LaTeX
$$$\\\\forall x \\\\in \\\\alpha, \\\\forall z \\\\in \\\\mathbb{Z}, \\\\left|x - \\\\operatorname{round} x\\\\right| \\\\le \\\\left|x - z\\\\right|.$$$
Lean4
theorem round_le (x : α) (z : ℤ) : |x - round x| ≤ |x - z| :=
by
rw [abs_sub_round_eq_min, min_le_iff]
rcases le_or_gt (z : α) x with (hx | hx) <;> [left; right]
· conv_rhs => rw [abs_eq_self.mpr (sub_nonneg.mpr hx), ← fract_add_floor x, add_sub_assoc]
simpa only [le_add_iff_nonneg_right, sub_nonneg, cast_le] using le_floor.mpr hx
· rw [abs_eq_neg_self.mpr (sub_neg.mpr hx).le]
conv_rhs => rw [← fract_add_floor x]
rw [add_sub_assoc, add_comm, neg_add, neg_sub, le_add_neg_iff_add_le, sub_add_cancel, le_sub_comm]
norm_cast
exact floor_le_sub_one_iff.mpr hx
