sq_lt_sq'

Mathlib.Algebra.Order.Ring.Abs

URI: https://scilib.ai/kg/mathlib#sq_lt_sq'

English

If -b < a and a < b, then a^2 < b^2.

Русский

Если -b < a и a < b, то a^2 < b^2.

LaTeX

$$$(-b < a) \\land (a < b) \\Rightarrow a^2 < b^2$$$

Lean4

theorem sq_lt_sq' (h1 : -b < a) (h2 : a < b) : a ^ 2 < b ^ 2 :=
  sq_lt_sq.2 (lt_of_lt_of_le (abs_lt.2 ⟨h1, h2⟩) (le_abs_self _))

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

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

Разделы

Аффилиация

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