toDFinsupp — Mathlib

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 _ _ _

Похожие утверждения