equivDFinsupp — Mathlib

English

The map converting multisets to DFinsupp and back is an additive equivalence between Multiset α and DFinsupp.

Русский

Обратимое по сложению отображение между Multiset α и DFinsupp, переводя мультимножество к DFinsupp и обратно.

LaTeX

$$$$ \\text{equivDFinsupp} : \\operatorname{Multiset}\\,\\alpha \\simeq_+ \\Pi_0 a:\\alpha, \\mathbb{N} $$$$

Lean4

/-- `Multiset.toDFinsupp` as an `AddEquiv`. -/
@[simps! apply symm_apply]
def equivDFinsupp : Multiset α ≃+ Π₀ _ : α, ℕ :=
  AddMonoidHom.toAddEquiv Multiset.toDFinsupp DFinsupp.toMultiset (by ext; simp) (by ext; simp)

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