abs_sub_lt_of_lt_lt

Mathlib.Algebra.Order.Group.Unbundled.Int

URI: https://scilib.ai/kg/mathlib#Int.abs_sub_lt_of_lt_lt

English

If m,a,b are natural with a < m and b < m, then |b − a| < m.

Русский

Если m,a,b ∈ ℕ и a < m, b < m, то |b − a| < m.

LaTeX

$$$ \text{If } a,b,m \in \mathbb{N},\ a < m,\ b < m\ \text{then } |b - a| < m. $$$

Lean4

theorem abs_sub_lt_of_lt_lt {m a b : ℕ} (ha : a < m) (hb : b < m) : |(b : ℤ) - a| < m := by rw [abs_lt]; cutsat

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru