zero_zpow_def — Mathlib

English

For any integer n, the n-th power of 0 in ENNReal is 1 if n=0, 0 if n>0, and ∞ if n<0.

Русский

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

LaTeX

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

Lean4

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

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