natAbs_le_iff_mul_self_le

Mathlib.Data.Int.Order.Lemmas

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

← MathLib Explorer

English

For all a,b ∈ ℤ, a.natAbs ≤ b.natAbs if and only if a^2 ≤ b^2.

Русский

Для любых a,b ∈ ℤ верно: |a| ≤ |b| эквивалентно a^2 ≤ b^2.

LaTeX

$$$\forall a,b \in \mathbb{Z}, a.\mathrm{natAbs} \le b.\mathrm{natAbs} \iff a^2 \le b^2.$$$

Lean4

theorem natAbs_le_iff_mul_self_le {a b : ℤ} : a.natAbs ≤ b.natAbs ↔ a * a ≤ b * b :=
  by
  rw [← abs_le_iff_mul_self_le, abs_eq_natAbs, abs_eq_natAbs]
  exact Int.ofNat_le.symm

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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