English
There is an order isomorphism between the finitely supported Nat-valued functions and multisets given by Finsupp.toMultiset, with the inverse given by Multiset.toFinsupp.
Русский
Существует упорядоченное изоморфизм между функциями с конечной опорой в ℕ и мультимножест-вами, заданный через Finsupp.toMultiset и обратное преобразование Multiset.toFinsupp.
LaTeX
$$$\mathrm{orderIsoMultiset} : (\alpha \to_0 \mathbb{N}) \simeq_o \mathrm{Multiset}\,\alpha$$$
Lean4
/-- `Finsupp.toMultiset` as an order isomorphism. -/
def orderIsoMultiset [DecidableEq ι] : (ι →₀ ℕ) ≃o Multiset ι
where
toEquiv := Multiset.toFinsupp.symm.toEquiv
map_rel_iff' {f g} := by simp [le_def, Multiset.le_iff_count]
