English
For any predicate p on α and f: ∀ a, p a → β, for s a multiset of α, we have pmap f s H = s.attach.map (λ x, f x.1 (H x.2)), i.e., pmap corresponds to mapping over the attachment with the witness facts.
Русский
Для любого предиката p на α и f: ∀ a, p a → β, для мультимножества s верно pmap f s H = s.attach.map (λ x, f x.1 (H x.2)); то есть pmap эквивалентно отображению по прикреплению с учетом доказательств.
LaTeX
$$$\\forall p:\\\\alpha\\\\to\\\\mathrm{Prop},\\; f:\\\\forall a,\\\\ p a\\\\to\\\\beta,\\; s:\\\\mathrm{Multiset}\\\\ \\alpha,\\; \\forall H:\\\\forall a\\\\in s,\\\\ p a,\\\\ \\mathrm{pmap}\\\\ f\\\\ s\\\\ H = s.\\\\attach.map\\\\ (\\\\lambda x\\\\, f x.1 (H x.2)).$$
Lean4
theorem pmap_eq_map_attach {p : α → Prop} (f : ∀ a, p a → β) (s) :
∀ H, pmap f s H = s.attach.map fun x => f x.1 (H _ x.2) :=
Quot.inductionOn s fun _ H => congr_arg _ <| List.pmap_eq_map_attach H
