English
There is a natural equivalence between a multiset m and the Finset of its enumeration, via the coeEmbedding.
Русский
Существует естественное эквивалентное отображение между мультимножством m и Finset его перечисления через отображение coeEmbedding.
LaTeX
$$coeEquiv (m : Multiset α) : m ≃ m.toEnumFinset$$
Lean4
/-- Another way to coerce a `Multiset` to a type is to go through `m.toEnumFinset` and coerce
that `Finset` to a type. -/
@[simps]
def coeEquiv (m : Multiset α) : m ≃ m.toEnumFinset
where
toFun
x :=
⟨m.coeEmbedding x, by
rw [Multiset.mem_toEnumFinset]
exact x.2.2⟩
invFun
x :=
⟨x.1.1, x.1.2, by
rw [← Multiset.mem_toEnumFinset]
exact x.2⟩
