English
Let s be a Sym α n and x an element of α. The attach of the extended symmetrized term cons(x, s) is exactly the cons of the head witness for x together with the attach of s, where every element of s is re-labeled to witness its membership in the enlarged multiset.
Русский
Пусть s ∈ Sym α n и x ∈ α. Тогда attaching(cons(x, s)) равняется конусу с головным элементом ⟨x, доказательство того, что x принадлежит x ∪ s⟩ и с хвостом, полученным из attach(s), где каждому элементу хвоста сопоставляется свидетельство принадлежности к расширенному мультисету.
LaTeX
$$$ (\\operatorname{attach}(\\operatorname{cons}(x,s))) = \\operatorname{cons}(\\langle x, \\operatorname{mem\\_cons\\_self}(x) \\rangle)\\big( \\operatorname{attach}(s) \\mapsto \\langle \\text{val}, \\operatorname{mem\\_cons\\_of\\_mem}(\\text{val}.\\text{prop}) \\rangle \\big) $$$
Lean4
@[simp]
theorem attach_cons (x : α) (s : Sym α n) :
(cons x s).attach = cons ⟨x, mem_cons_self _ _⟩ (s.attach.map fun x => ⟨x, mem_cons_of_mem x.prop⟩) :=
coe_injective <| Multiset.attach_cons _ _
