to_ofNatMultiset — Mathlib

English

The natural multiset corresponding to the prime multiset constructed from a Nat multiset is exactly the original Nat multiset.

Русский

Естественное отображение обратно возвращает исходное мультимножество Nat.

LaTeX

$$$ (\\operatorname{ofNatMultiset}(v,h) : \\operatorname{Multiset}\\mathbb{N}) = v $$$

Lean4

theorem to_ofNatMultiset (v : Multiset ℕ) (h) : (ofNatMultiset v h : Multiset ℕ) = v :=
  by
  dsimp [ofNatMultiset, toNatMultiset]
  rw [Multiset.map_pmap, Multiset.pmap_eq_map, Multiset.map_id']

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