abs_le_of_sq_le_sq

Mathlib.Algebra.Order.Ring.Abs

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

English

If a^2 ≤ b^2 and 0 ≤ b, then |a| ≤ b.

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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