pow_lt_pow_left_iff

Mathlib.Data.ENNReal.Operations

URI: https://scilib.ai/kg/mathlib#ENNReal.pow_lt_pow_left_iff

English

For any a,b in ENNReal and n ≠ 0, a^n < b^n iff a < b.

Русский

Для любых a,b ∈ ENNReal и n ≠ 0 верно: a^n < b^n тогда и только тогда, когда a < b.

LaTeX

$$$\forall a,b \in ENNReal, \; \forall n \in \mathbb{N}, \; n \neq 0 \Rightarrow a^n < b^n \;\iff\; a < b$$$

Lean4

protected theorem pow_lt_pow_left_iff {n : ℕ} (hn : n ≠ 0) : a ^ n < b ^ n ↔ a < b :=
  (ENNReal.pow_right_strictMono hn).lt_iff_lt

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

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

Разделы

Аффилиация

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