English
Attach associates a proof that each element belongs to s to each coordinate, producing an element of the symmetric power on {x | x ∈ s}.
Русский
Attach добавляет доказательство принадлежности каждому элементу множества s к каждому координату, образуя элемент Sym на {x | x ∈ s}.
LaTeX
$$$\\mathrm{attach}(s) : \\mathrm{Sym}(\\{ x \\mid x \\in s \\}, n) \\text{ with underlying structure } \\langle s.value.\\mathrm{attach}, \\ldots \\rangle.$$$
Lean4
/-- "Attach" a proof that `a ∈ s` to each element `a` in `s` to produce
an element of the symmetric power on `{x // x ∈ s}`. -/
def attach (s : Sym α n) : Sym { x // x ∈ s } n :=
⟨s.val.attach, by (conv_rhs => rw [← s.2, ← Multiset.card_attach])⟩
