English
Let p be a predicate on α and f assign to each a an element β whenever p(a) holds. For a multiset a :: m and a witness h that p holds for every element of a :: m, the mapped multiset pmap f (a ::ₘ m) h is equal to the cons of f a (h a (mem_cons_self a m)) with pmap f m on the appropriately transformed witness.
Русский
Пусть p — предикат на α, и пусть f отображает каждый элемент a при условии p(a) в элемент β. Для мультимножества a ::ₘ m и доказательства h того, что p верно для всех элементов a :: m, отображение pmap f на (a ::ₘ m) с доказательством h равно конструированному списку, состоящему из f a (h a (mem_cons_self a m)) и продолжения pmap f m с преобразованным доказательством.
LaTeX
$$$\forall {p : \alpha \to \text{Prop}},\ f : \forall a, p(a) \to \beta,\ a : \alpha,\ m : Multiset\,\alpha,\ h : \forall b \in a ::ₘ m, p(b) \,\Rightarrow \\ pmap f (a ::ₘ m) h = f\ a\ (h\ a\ (mem_cons_self\ a\ m)) ::ₘ pmap f\ m (\lambda a' \ ha' , h\ a' (mem_cons_of_mem ha'))$$$
Lean4
@[simp]
theorem pmap_cons {p : α → Prop} (f : ∀ a, p a → β) (a : α) (m : Multiset α) :
∀ h : ∀ b ∈ a ::ₘ m, p b,
pmap f (a ::ₘ m) h = f a (h a (mem_cons_self a m)) ::ₘ pmap f m fun a ha => h a <| mem_cons_of_mem ha :=
Quotient.inductionOn m fun _l _h => rfl
