toMultiset_toDFinsupp — Mathlib

English

The bijection between Multiset α and DFinsupp α is inverse to toMultiset and toDFinsupp.

Русский

Существуют биекции между Multiset α и DFinsupp α, образующие взаимно обратные отображения toMultiset и toDFinsupp.

LaTeX

$$$$ \\text{toMultiset} \\circ \\text{toDFinsupp} = \\mathrm{id}, \\quad \\text{toDFinsupp} \\circ \\text{toMultiset} = \\mathrm{id} $$$$

Lean4

@[simp]
theorem toMultiset_toDFinsupp (f : Π₀ _ : α, ℕ) : Multiset.toDFinsupp (DFinsupp.toMultiset f) = f :=
  Multiset.equivDFinsupp.apply_symm_apply f

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