univ_pow — Mathlib

English

Let α be a finite type. Then for every natural number n ≥ 1, the n-th product of the universal finite set with itself equals the universal finite set: (univ : Finset α)^n = univ.

Русский

Пусть α — конечный тип. Тогда для любого n ≥ 1 выполняется (univ : Finset α)^n = univ; то есть объединение всех n-словых произведений элементов α даёт весь α.

LaTeX

$$$(\mathrm{univ}_{\alpha})^n = \mathrm{univ}_{\alpha}$, \quad n > 0, \; \alpha \text{ конечен}$$$

Lean4

@[to_additive (attr := simp) nsmul_univ]
theorem univ_pow [Fintype α] (hn : n ≠ 0) : (univ : Finset α) ^ n = univ :=
  coe_injective <| by rw [coe_pow, coe_univ, Set.univ_pow hn]

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