sq_le_sq'

Mathlib.Algebra.Order.Ring.Abs

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

English

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

Русский

Если -b ≤ a и a ≤ b, то a^2 ≤ b^2.

LaTeX

$$$(-b \\le a) \\land (a \\le b) \\Rightarrow a^2 \\le b^2$$$

Lean4

theorem sq_le_sq' (h1 : -b ≤ a) (h2 : a ≤ b) : a ^ 2 ≤ b ^ 2 :=
  sq_le_sq.2 (le_trans (abs_le.mpr ⟨h1, h2⟩) (le_abs_self _))

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

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

Разделы

Аффилиация

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