English
The count of p on the image map f s equals the card of the subset of s where p holds after applying f.
Русский
Подсчёт p на отображении f s равен кардиналу подмножества s, где p (f a) истинно.
LaTeX
$$$\operatorname{countP} p (\operatorname{map} f s) = \operatorname{card}(s.filter (\lambda a. p (f a)))$$$
Lean4
theorem countP_map (f : α → β) (s : Multiset α) (p : β → Prop) [DecidablePred p] :
countP p (map f s) = card (s.filter fun a => p (f a)) :=
by
refine Multiset.induction_on s ?_ fun a t IH => ?_
· rw [map_zero, countP_zero, filter_zero, card_zero]
· rw [map_cons, countP_cons, IH, filter_cons, card_add, apply_ite card, card_zero, card_singleton, Nat.add_comm]
