eq_top_of_pow

Mathlib.Data.ENNReal.Operations

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

English

If a^n = ∞, then a = ∞.

Русский

Если a^n = ∞, то a = ∞.

LaTeX

$$$a^{n} = \infty \Rightarrow a = \infty$$$

Lean4

theorem eq_top_of_pow (n : ℕ) (ha : a ^ n = ∞) : a = ∞ :=
  WithTop.eq_top_of_pow n ha

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

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

Разделы

Аффилиация

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