sq_lt_one_iff_abs_lt_one

Mathlib.Algebra.Order.Ring.Abs

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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