abs_le_iff_mul_self_le

Mathlib.Algebra.Order.Ring.Abs

URI: https://scilib.ai/kg/mathlib#abs_le_iff_mul_self_le

← MathLib Explorer

English

For all a,b, |a| ≤ |b| iff a^2 ≤ b^2.

Русский

Для всех a,b: |a| ≤ |b| тогда и только тогда, когда a^2 ≤ b^2.

LaTeX

$$$|a| \le |b| \iff a^{2} \le b^{2}$$$

Lean4

theorem abs_le_iff_mul_self_le : |a| ≤ |b| ↔ a * a ≤ b * b :=
  by
  rw [← abs_mul_abs_self, ← abs_mul_abs_self b]
  exact mul_self_le_mul_self_iff (abs_nonneg a) (abs_nonneg b)

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

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

Разделы

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

Аффилиация

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