coeMultisetPNatNat — Mathlib

English

There is a canonical map from multisets of positive naturals to multisets of naturals obtained by replacing each element by its natural value; this defines a natural inclusion of multisets.

Русский

Существует каноническое отображение из мультимножества положительных натуральных чисел в мультимножество натуральных чисел, получаемое заменой каждого элемента его натуральным значением; это определяет естественное включение мультимножества.

LaTeX

$$$ f: \\operatorname{Multiset}(\\mathbb{N}_{+}) \\to \\operatorname{Multiset}(\\mathbb{N}), \\quad f(v) = \\operatorname{map}(\\mathsf{val})\,v $$$

Lean4

instance coeMultisetPNatNat : Coe (Multiset ℕ+) (Multiset ℕ) :=
  ⟨fun v => v.map (↑)⟩

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