sq_le_one_iff_abs_le_one

Mathlib.Algebra.Order.Ring.Abs

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

English

For any a, a^2 ≤ 1 iff |a| ≤ 1.

Русский

Для любого a: a^2 ≤ 1 эквивалентно |a| ≤ 1.

LaTeX

$$$a^2 \\le 1 \\iff |a| \\le 1$$$

Lean4

@[simp]
theorem sq_le_one_iff_abs_le_one (a : α) : a ^ 2 ≤ 1 ↔ |a| ≤ 1 := by
  simpa only [one_pow, abs_one] using sq_le_sq (a := a) (b := 1)

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

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

Разделы

Аффилиация

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