English
There exists a natural order isomorphism between multisets and finitely supported ℕ-valued functions, given by toFinsupp and its inverse toMultiset.
Русский
Существует естественная упорядоченная биекция между мультимножества и функциями с конечной опорой, заданная через toFinsupp и обратное преобразование toMultiset.
LaTeX
$$$\mathrm{toFinsupp} : \mathrm{Multiset}\,\alpha \simeq_o (\alpha \to_0 \mathbb{N})$$$
Lean4
/-- Given a multiset `s`, `s.toFinsupp` returns the finitely supported function on `ℕ` given by
the multiplicities of the elements of `s`. -/
@[simps symm_apply]
def toFinsupp : Multiset α ≃+ (α →₀ ℕ)
where
toFun s := ⟨s.toFinset, fun a => s.count a, fun a => by simp⟩
invFun f := Finsupp.toMultiset f
map_add' _ _ := Finsupp.ext fun _ => count_add _ _ _
right_inv
f :=
Finsupp.ext fun a =>
by
simp only [Finsupp.toMultiset_apply, Finsupp.sum, Multiset.count_sum', Multiset.count_singleton, mul_boole,
Finsupp.coe_mk, Finsupp.mem_support_iff, Multiset.count_nsmul, Finset.sum_ite_eq, ite_not, ite_eq_right_iff]
exact Eq.symm
left_inv
s := by simp only [Finsupp.toMultiset_apply, Finsupp.sum, Finsupp.coe_mk, Multiset.toFinset_sum_count_nsmul_eq]
