top_pow — Mathlib

English

The top raised to a natural power is top: for any nonzero n, ⊤^n = ⊤.

Русский

Верхний фильтр возводится в известную натуральную степень: для любого ненулевого n получается ⊤^n = ⊤.

LaTeX

$$$\forall n \in \mathbb{N},\ n \neq 0 \Rightarrow (\top : \mathrm{Filter}(\alpha))^n = \top.$$$

Lean4

@[to_additive nsmul_top]
theorem top_pow : ∀ {n : ℕ}, n ≠ 0 → (⊤ : Filter α) ^ n = ⊤
  | 0 => fun h => (h rfl).elim
  | 1 => fun _ => pow_one _
  | n + 2 => fun _ => by rw [pow_succ, top_pow n.succ_ne_zero, top_mul_top]

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