lt_of_mul_self_lt_mul_self₀

Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic

URI: https://scilib.ai/kg/mathlib#lt_of_mul_self_lt_mul_self₀

English

If a,b ≥ 0 and a·a < b·b, then a < b.

Русский

Если a,b ≥ 0 и a^2 < b^2, то a < b.

LaTeX

$$$0 \le a \land 0 \le b \land a\cdot a < b\cdot b \Rightarrow a < b$$$

Lean4

theorem lt_of_mul_self_lt_mul_self₀ (hb : 0 ≤ b) : a * a < b * b → a < b :=
  by
  simp only [← sq]
  exact lt_of_pow_lt_pow_left₀ _ hb

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

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

Разделы

Аффилиация

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