sym_univ — Mathlib

English

If α is finite, then the nth symmetric power of the universal finite set equals the universal finite set in the corresponding type.

Русский

Если α конечна, то n-ая симметрическая мощность универсума множества α равна универсуму соответствующего типа.

LaTeX

$$$ (\\mathrm{univ})^{(n)} = \\mathrm{univ}$$$

Lean4

@[simp]
theorem sym_univ [Fintype α] (n : ℕ) : (univ : Finset α).sym n = univ :=
  eq_univ_iff_forall.2 fun _s ↦ mem_sym_iff.2 fun _a _ ↦ mem_univ _

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