English
The support of esymm is the biUnion over n-element subsets of univ of the supports of the corresponding monomials.
Русский
Опор esymm есть биобъединение по всем n-элементным подмножествам множества переменных.
LaTeX
$$$ \\operatorname{support}(\\text{esymm}(\\sigma,R,n)) = (\\mathrm{powersetCard}\\; n\\; (\\mathrm{univ})).\\mathrm{biUnion} \\; (\\\\lambda t, (\\\\mathrm{Finsupp}.single (\\\\sum i \\,\\\\in t, \\\\mathrm{Finsupp.single i 1}) (1)) .\\\\operatorname{support})$$$
Lean4
theorem support_esymm'' [DecidableEq σ] [Nontrivial R] (n : ℕ) :
(esymm σ R n).support =
(powersetCard n (univ : Finset σ)).biUnion fun t =>
(Finsupp.single (∑ i ∈ t, Finsupp.single i 1) (1 : R)).support :=
by
rw [esymm_eq_sum_monomial]
simp only [← single_eq_monomial]
refine Finsupp.support_sum_eq_biUnion (powersetCard n (univ : Finset σ)) ?_
intro s t hst
rw [disjoint_left, Finsupp.support_single_ne_zero _ one_ne_zero]
rw [Finsupp.support_single_ne_zero _ one_ne_zero]
simp only [mem_singleton]
rintro a h rfl
have := congr_arg Finsupp.support h
rw [Finsupp.support_sum_eq_biUnion, Finsupp.support_sum_eq_biUnion] at this
· have hsingle : ∀ s : Finset σ, ∀ x : σ, x ∈ s → (Finsupp.single x 1).support = { x } :=
by
intro _ x _
rw [Finsupp.support_single_ne_zero x one_ne_zero]
have hs := biUnion_congr (of_eq_true (eq_self s)) (hsingle s)
have ht := biUnion_congr (of_eq_true (eq_self t)) (hsingle t)
rw [hs, ht] at this
· simp only [biUnion_singleton_eq_self] at this
exact absurd this hst.symm
all_goals intro x y; simp [Finsupp.support_single_disjoint]
