English
Let p be a predicate on α and f: α → p(a) → β. For any multiset s, the multiset pmap f s H equals the ordinary map of the function a ↦ f a (with H providing the needed witnesses). In other words, pmap f s H = map f s interpreted pointwise.
Русский
Пусть p — предикат на α и f: α → p(a) → β. Для любого мультимножества s отображение pmap f s H эквивалентно обычному отображению функции a ↦ f a на s, где H обеспечивает нужные доказательства. Другими словами, pmap f s H = map f s поэлементно.
LaTeX
$$$\\forall p:\\\\alpha\\\\to\\\\mathrm{Prop},\\; f:\\\\alpha\\\\to (p\\\\ a)\\\\to\\\\beta,\\; s:\\\\mathrm{Multiset}\\\\ \\alpha,\\; \\forall H:\\\\forall a\\\\in s,\\\\ p a,\\\\ pmap f s H = map f s.$$
Lean4
theorem pmap_eq_map (p : α → Prop) (f : α → β) (s : Multiset α) : ∀ H, @pmap _ _ p (fun a _ => f a) s H = map f s :=
Quot.inductionOn s fun _ H => congr_arg _ <| List.pmap_eq_map H
