English
If you convert a multiset of naturals (primes) to a multiset of positive naturals and back, you recover the original multiset of naturals.
Русский
Преобразование обратно восстанавливает исходное мультимножество простых.
LaTeX
$$$ (v : \\operatorname{Multiset}\\mathbb{N}_{+}) (h) : (\\operatorname{ofPNatMultiset}(v,h) : \\operatorname{Multiset}\\mathbb{N}_{+}) = v $$$
Lean4
theorem to_ofPNatMultiset (v : Multiset ℕ+) (h) : (ofPNatMultiset v h : Multiset ℕ+) = v :=
by
dsimp [ofPNatMultiset, toPNatMultiset]
have : (fun (p : ℕ+) (h : p.Prime) => ((↑) : Nat.Primes → ℕ+) ⟨p, h⟩) = fun p _ => id p :=
by
funext p h
apply Subtype.eq
rfl
rw [Multiset.map_pmap, this, Multiset.pmap_eq_map, Multiset.map_id]
