eq_of_abs_lt — Mathlib

English

Let m, a, b be natural numbers. If a is congruent to b modulo m and the absolute difference |b − a| is less than m, then a = b.

Русский

Пусть m, a, b — натуральные числа. Если a ≡ b (mod m) и |b − a| < m, то a = b.

LaTeX

$$$\\\\forall m\\\\, a\\\\, b \\\\in \\\\mathbb{N},\\\\ a \\\\\\equiv b \\\\pmod{m} \\\\land \\\\left|b - a\\\\right| < m \\\\Rightarrow \\\\ a = b$$$

Lean4

theorem eq_of_abs_lt (h : a ≡ b [MOD m]) (h2 : |(b : ℤ) - a| < m) : a = b :=
  by
  apply Int.ofNat.inj
  rw [eq_comm, ← sub_eq_zero]
  exact Int.eq_zero_of_abs_lt_dvd h.dvd h2

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