natAbs_le_iff_sq_le — Mathlib

English

For integers a,b, the non-strict inequality of absolute values is equivalent to the non-strict inequality of their squares.

Русский

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

LaTeX

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

Lean4

theorem natAbs_le_iff_sq_le {a b : ℤ} : a.natAbs ≤ b.natAbs ↔ a ^ 2 ≤ b ^ 2 :=
  by
  rw [sq, sq]
  exact natAbs_le_iff_mul_self_le

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