zpow_pos — Mathlib

English

If a ≠ 0 and a ≠ ∞, then for every integer n, a^n > 0.

Русский

Если a ≠ 0 и a ≠ ∞, то для любого целого n имеем a^n > 0.

LaTeX

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

Lean4

theorem zpow_pos (ha : a ≠ 0) (h'a : a ≠ ∞) (n : ℤ) : 0 < a ^ n :=
  by
  cases n
  · simpa using ENNReal.pow_pos ha.bot_lt _
  · simp only [h'a, pow_eq_top_iff, zpow_negSucc, Ne, ENNReal.inv_pos, false_and, not_false_eq_true]

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