count_filter — Mathlib

English

The count of a in the filter equals either the original count or zero, depending on whether P(a) holds.

Русский

Счёт элемента в фильтре равен либо исходному счёту, либо нулю, в зависимости от того, выполняется ли P(a).

LaTeX

$$$\operatorname{count} a (\operatorname{filter} p s) = \begin{cases} \operatorname{count} a s, & p(a) \\ 0, & \lnot p(a) \end{cases}$$$

Lean4

theorem count_filter {p} [DecidablePred p] {a} {s : Multiset α} : count a (filter p s) = if p a then count a s else 0 :=
  by
  split_ifs with h
  · exact count_filter_of_pos h
  · exact count_filter_of_neg h

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