English
Let s be an element of Sym α (n+1) and a ∈ α with h: a ∈ s. Then erase(s,a,h) is an element of Sym α n whose underlying multiset is s.val.erase a; in particular, the cardinality is n.
Русский
Пусть s ∈ Sym α (n+1) и a ∈ α such that a ∈ s. Тогда erase(s,a,h) ∈ Sym α n имеет основание как s.val.erase a; следовательно, кардинальность равна n.
LaTeX
$$$ (\mathrm{Sym.erase}(s,a,h)).toMultiset = s.toMultiset.erase a \quad\text{and}\quad \operatorname{card}((\mathrm{Sym.erase}(s,a,h)).toMultiset) = n. $$$
Lean4
/-- `erase s a h` is the sym that subtracts 1 from the
multiplicity of `a` if a is present in the sym. -/
def erase [DecidableEq α] (s : Sym α (n + 1)) (a : α) (h : a ∈ s) : Sym α n :=
⟨s.val.erase a, (Multiset.card_erase_of_mem h).trans <| s.property.symm ▸ n.pred_succ⟩
