top_zpow_def — Mathlib

English

For any integer n, ∞^n equals 1 if n=0, ∞ if n>0, and 0 if n<0.

Русский

Для любого целого n, ∞^n равно 1 если n=0, ∞ если n>0, и 0 если n<0.

LaTeX

$$$\\forall n \\in \\mathbb{Z},\\; (\\top : \\mathbb{R}_{\\ge 0}^{\\infty})^n = \\begin{cases} 1 & (n=0), \\\\ \\top & (n>0), \\\\ 0 & (n<0). \\end{cases}$$$

Lean4

theorem top_zpow_def (n : ℤ) : (⊤ : ℝ≥0∞) ^ n = if n = 0 then 1 else if 0 < n then ⊤ else 0 := by
  obtain ((_ | n) | n) := n <;> simp [-Nat.cast_add, -Int.natCast_add]

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