zpow_lt_top — Mathlib

English

If a ≠ 0 and a ≠ ∞, then for any integer n, a^n < ∞.

Русский

Если a ≠ 0 и a ≠ ∞, то для любого n выполняется a^n < ∞.

LaTeX

$$$\\forall a \\in \\mathbb{R}_{\\ge 0}^{\\infty},\\; a \\neq 0 \\land a \\neq \\infty \\Rightarrow ∀ n ∈ \\mathbb{Z}, a^n < \\infty$$$

Lean4

theorem zpow_lt_top (ha : a ≠ 0) (h'a : a ≠ ∞) (n : ℤ) : a ^ n < ∞ :=
  by
  cases n
  · simpa using ENNReal.pow_lt_top h'a.lt_top
  · simp only [ENNReal.pow_pos ha.bot_lt, zpow_negSucc, inv_lt_top]

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