English
Mapping a multiset by a predicate and counting True equals the cardinality of the predicate-filtered multiset.
Русский
Отображение мультисета через предикат и подсчёт True эквивалентно мощности фильтрованного по предикату множества.
LaTeX
$$$ (s.map p).count True = \\mathrm{card}(s.filter p) $$$
Lean4
/-- Mapping a multiset through a predicate and counting the `True`s yields the cardinality of the set
filtered by the predicate. Note that this uses the notion of a multiset of `Prop`s - due to the
decidability requirements of `count`, the decidability instance on the LHS is different from the
RHS. In particular, the decidability instance on the left leaks `Classical.decEq`.
See [here](https://github.com/leanprover-community/mathlib/pull/11306#discussion_r782286812)
for more discussion.
-/
@[simp]
theorem map_count_True_eq_filter_card (s : Multiset α) (p : α → Prop) [DecidablePred p] :
(s.map p).count True = card (s.filter p) := by
simp only [count_eq_card_filter_eq, filter_map, card_map, Function.id_comp, eq_true_eq_id, Function.comp_apply]
