countP_filter — Mathlib

English

Filtering by q and counting with p equals counting with p on the filtered and filtered-by-not-q parts.

Русский

Фильтрация по q и подсчёт по p равны подсчёту p по отфильтрованному и не-q-частям.

LaTeX

$$$\operatorname{countP} p (\operatorname{filter} q s) = \operatorname{countP}(\lambda a. p a \land q a) s$$$

Lean4

@[simp]
theorem countP_filter (q) [DecidablePred q] (s : Multiset α) : countP p (filter q s) = countP (fun a => p a ∧ q a) s :=
  by simp [countP_eq_card_filter]

Похожие утверждения