abs_lt_of_sq_lt_sq'

Mathlib.Algebra.Order.Ring.Abs

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

English

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

Русский

Если a^2 < b^2 и 0 ≤ b, тогда -b < a и a < b.

LaTeX

$$$a^2 < b^2 \\land 0 \\le b \\Rightarrow -b < a \\land a < b$$$

Lean4

theorem abs_lt_of_sq_lt_sq' (h : a ^ 2 < b ^ 2) (hb : 0 ≤ b) : -b < a ∧ a < b :=
  abs_lt.1 <| abs_lt_of_sq_lt_sq h hb

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

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

Разделы

Аффилиация

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