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 |a| < b.

Русский

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

LaTeX

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

Lean4

theorem abs_lt_of_sq_lt_sq (h : a ^ 2 < b ^ 2) (hb : 0 ≤ b) : |a| < b := by rwa [← abs_of_nonneg hb, ← sq_lt_sq]

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

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

Разделы

Аффилиация

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