English
For α, n, a ∈ α and s ∈ Sym α n, we have Sym.cons'(a, s) equals the corresponding transformed element under the equivalence with the Sym' construction.
Русский
Для α, n, a ∈ α и s ∈ Sym α n выполняется равенство Sym.cons'(a, s) равняется соответствующему элементу после применения эквивалентности к конструкту Sym'.
LaTeX
$$$ \mathrm{cons'}(a, \mathrm{Equiv}(s)) = \mathrm{Equiv}(\mathrm{cons}(a, s)). $$$
Lean4
/-- Multisets of cardinality n are equivalent to length-n vectors up to permutations.
-/
def symEquivSym' {α : Type*} {n : ℕ} : Sym α n ≃ Sym' α n :=
Equiv.subtypeQuotientEquivQuotientSubtype _ _ (fun _ => by rfl) fun _ _ => by rfl
