support_esymm — Mathlib

English

The support of esymm equals the image of the map t ↦ ∑ i∈t Finsupp.single i 1 on the powersetCard n (univ).

Русский

Опора esymm равна образу отображения t ↦ ∑ i∈t e_i на powersetCard n(univ).

LaTeX

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

Lean4

theorem support_esymm [DecidableEq σ] [Nontrivial R] (n : ℕ) :
    (esymm σ R n).support = (powersetCard n (univ : Finset σ)).image fun t => ∑ i ∈ t, Finsupp.single i 1 :=
  by
  rw [support_esymm']
  exact biUnion_singleton

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