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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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