English
Let p be a predicate on α, g: β → γ, and f: ∀ a, p a → β. For any s, the equality map g (pmap f s H) = pmap (λ a h, g (f a h)) s H holds, i.e., mapping after pmap is the same as pmap of the mapped generator.
Русский
Пусть p — предикат на α, g: β → γ и f: ∀ a, p a → β. Для любого s верно равенство map g (pmap f s H) = pmap (λ a h, g (f a h)) s H: отображение после pmap эквивалентно pmap отображения после применения g к результату f.
LaTeX
$$$\\forall p:\\\\alpha\\\\to\\\\mathrm{Prop},\\; g:\\\\beta\\\\to\\\\gamma,\\; f:\\\\forall a,\\\\ p a\\\\to\\\\beta,\\; s:\\\\mathrm{Multiset}\\\\ \\alpha,\\; \\forall H:\\\\forall a\\\\in s,\\\\ p a,\\\\ \\mathrm{map}\\\\ g\\\\ (\\\\mathrm{pmap}\\\\ f\\\\ s\\\\ H) = \\\\mathrm{pmap}\\\\ (\\\\lambda a\\\\,\\\\ h\\\\,\\\\ g (f a h))\\\\ s\\\\ H.$$
Lean4
theorem map_pmap {p : α → Prop} (g : β → γ) (f : ∀ a, p a → β) (s) :
∀ H, map g (pmap f s H) = pmap (fun a h => g (f a h)) s H :=
Quot.inductionOn s fun _ H => congr_arg _ <| List.map_pmap H
