support_esymm' — Mathlib

English

The support of esymm is the biUnion over n-element subsets t of univ of the singleton {∑_{i∈t} e_i}.

Русский

Опора esymm — биобъединение по всем n-элементным подмножествам t: {∑_{i∈t} e_i}.

LaTeX

$$$ \\operatorname{support}(\\text{esymm}(\\sigma,R,n)) = (\\mathrm{powersetCard}\\; n\\; (\\mathrm{univ})).\\mathrm{biUnion} \\; t \\mapsto \\{ \\sum i \\in t, Finsupp.single i 1 \\} $$$

Lean4

theorem support_esymm' [DecidableEq σ] [Nontrivial R] (n : ℕ) :
    (esymm σ R n).support = (powersetCard n (univ : Finset σ)).biUnion fun t => {∑ i ∈ t, Finsupp.single i 1} :=
  by
  rw [support_esymm'']
  congr
  funext
  exact Finsupp.support_single_ne_zero _ one_ne_zero

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