empty_pow — Mathlib

English

For any nonzero n, the nth power of the empty set is the empty set.

Русский

Для любого ненулевого n-го возведения множество пустое множества при возведении в степень.

LaTeX

$$$$ (\emptyset : Set \alpha)^n = \emptyset \quad (n > 0). $$$$

Lean4

@[to_additive (attr := simp) nsmul_empty]
theorem empty_pow (hn : n ≠ 0) : (∅ : Set α) ^ n = ∅ :=
  match n with
  | n + 1 => by simp [pow_succ]

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