English
If a is not in s, there is a natural equivalence between the nth symmetric power of insert a s and the disjoint union over i in Fin(n+1) of the (n−i)th symmetric power of s.
Русский
Если a не принадлежит s, существует естественная биекция между симметрической мощностью n элемента (insert a s) и дисжойн-объединением по i ∈ Fin(n+1) s^{(n−i)}.
LaTeX
$$$ (\\mathrm{sym}^n(\\mathrm{insert}\\ a\\ s)) \\simeq \\Sigma i: \\mathrm{Fin}(n+1), s^{(n-i)} $ при условии a ∉ s.$$
Lean4
theorem sym_fill_mem (a : α) {i : Fin (n + 1)} {m : Sym α (n - i)} (h : m ∈ s.sym (n - i)) :
m.fill a i ∈ (insert a s).sym n :=
mem_sym_iff.2 fun b hb ↦ mem_insert.2 <| (Sym.mem_fill_iff.1 hb).imp And.right <| mem_sym_iff.1 h b
