le_of_sq_le_sq

Mathlib.Algebra.Order.Ring.Abs

URI: https://scilib.ai/kg/mathlib#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 le_of_sq_le_sq (h : a ^ 2 ≤ b ^ 2) (hb : 0 ≤ b) : a ≤ b :=
  le_abs_self a |>.trans <| abs_le_of_sq_le_sq h hb

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

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

Разделы

Аффилиация

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