ofPNatMultiset — Mathlib

English

The prime multiset obtained from a Nat multiset via ofPNatMultiset maps back to the original multiset of primes.

Русский

Приматное мультимножество, полученное из Nat мультимножества через ofPNatMultiset, отображается обратно в исходное мультимножество простых.

LaTeX

$$$ (\\operatorname{ofPNatMultiset}(v,h) : \\operatorname{Multiset}\\mathbb{N}_{+}) = v $$$

Lean4

/-- If a `Multiset ℕ+` consists only of primes, it can be recast as a `PrimeMultiset`. -/
def ofPNatMultiset (v : Multiset ℕ+) (h : ∀ p : ℕ+, p ∈ v → p.Prime) : PrimeMultiset :=
  @Multiset.pmap ℕ+ Nat.Primes PNat.Prime (fun p hp => ⟨(p : ℕ), hp⟩) v h

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