English
There is a DFinsupp-valued map Multiset.toDFinsupp: Multiset α → Π₀ _ : α, ℕ, taking counts of each element.
Русский
Существует отображение Multiset.toDFinsupp: Multiset α → Π₀ a:α, ℕ, которое считает количество каждого элемента.
LaTeX
$$$$ \\text{toDFinsupp}: \\operatorname{Multiset}\\,\\alpha \\to \\Pi_0 a:\\alpha, \\mathbb{N} $$$$
Lean4
/-- A DFinsupp version of `Multiset.toFinsupp`. -/
def toDFinsupp : Multiset α →+ Π₀ _ : α, ℕ
where
toFun
s :=
{ toFun := fun n ↦ s.count n
support' := Trunc.mk ⟨s, fun i ↦ (em (i ∈ s)).imp_right Multiset.count_eq_zero_of_notMem⟩ }
map_zero' := rfl
map_add' _ _ := DFinsupp.ext fun _ ↦ Multiset.count_add _ _ _