eq_of_lt_of_lt — Mathlib

English

Let m, a, b be natural numbers. If a ≡ b (mod m) and a < m and b < m, then a = b.

Русский

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

LaTeX

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

Lean4

theorem eq_of_lt_of_lt (h : a ≡ b [MOD m]) (ha : a < m) (hb : b < m) : a = b :=
  h.eq_of_abs_lt <| Int.abs_sub_lt_of_lt_lt ha hb

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