pow_right_strictMono

Mathlib.Data.ENNReal.Operations

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

English

For any n ≠ 0, the map a ↦ a^n is strictly monotone on ENNReal.

Русский

Для любого n ≠ 0 отображение a ↦ a^n строго возрастает на ENNReal.

LaTeX

$$$\forall n \in \mathbb{N}, n \neq 0 \Rightarrow \text{StrictMono}(a \mapsto a^n)$$$

Lean4

protected theorem pow_right_strictMono {n : ℕ} (hn : n ≠ 0) : StrictMono fun a : ℝ≥0∞ ↦ a ^ n :=
  WithTop.pow_right_strictMono hn

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

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

Разделы

Аффилиация

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