lt_of_pow_lt_pow_left₀

Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic

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

English

If a ≥ 0 and a^n < b^n, then a < b.

Русский

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

LaTeX

$$$0 \le a \Rightarrow a^n < b^n \Rightarrow a < b$$$

Lean4

theorem lt_of_pow_lt_pow_left₀ (n : ℕ) (hb : 0 ≤ b) (h : a ^ n < b ^ n) : a < b :=
  lt_of_not_ge fun hn => not_lt_of_ge (pow_le_pow_left₀ hb hn _) h

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

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

Разделы

Аффилиация

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