pow_le_pow_left_iff

Mathlib.Data.ENNReal.Operations

URI: https://scilib.ai/kg/mathlib#ENNReal.pow_le_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 \le b^n \;\iff\; a \le b$$$

Lean4

protected theorem pow_le_pow_left_iff {n : ℕ} (hn : n ≠ 0) : a ^ n ≤ b ^ n ↔ a ≤ b :=
  (ENNReal.pow_right_strictMono hn).le_iff_le

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

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

Разделы

Аффилиация

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