pow_ne_top_iff

Mathlib.Data.ENNReal.Operations

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

English

a^n ≠ ∞ if and only if a ≠ ∞ or n = 0.

Русский

a^n ≠ ∞ тогда и только тогда, когда a ≠ ∞ или n = 0.

LaTeX

$$$a^{n} \neq \infty \iff a \neq \infty \lor n = 0$$$

Lean4

theorem pow_ne_top_iff : a ^ n ≠ ∞ ↔ a ≠ ∞ ∨ n = 0 :=
  WithTop.pow_ne_top_iff

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

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

Разделы

Аффилиация

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