le_of_pow_le_pow_left₀

Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic

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

← MathLib Explorer

English

If a^n ≤ b^n and a,b ≥ 0 with n>0, then a ≤ b.

Русский

Если a^n ≤ b^n и a,b ≥ 0 при n>0, то a ≤ b.

LaTeX

$$$n \neq 0 \land 0 \le a \land 0 \le b \land a^n \le b^n \Rightarrow a \le b$$$

Lean4

theorem le_of_pow_le_pow_left₀ (hn : n ≠ 0) (hb : 0 ≤ b) (h : a ^ n ≤ b ^ n) : a ≤ b :=
  le_of_not_gt fun h1 => not_le_of_gt (pow_lt_pow_left₀ h1 hb hn) h

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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