natAbs_lt_iff_sq_lt

Mathlib.Data.Int.Lemmas

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

English

For integers a,b, the strict inequality of absolute values corresponds to a strict inequality of their squares.

Русский

Для целых a, b неравенство модулей соответствует неравенству квадратов.

LaTeX

$$$\forall a,b \in \mathbb{Z},\ |a| < |b| \iff a^{2} < b^{2}$$$

Lean4

theorem natAbs_lt_iff_sq_lt {a b : ℤ} : a.natAbs < b.natAbs ↔ a ^ 2 < b ^ 2 :=
  by
  rw [sq, sq]
  exact natAbs_lt_iff_mul_self_lt

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

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

Разделы

Аффилиация

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