count_eq_count_filter_add — Mathlib

English

For any decidable predicate P over α, the count of a in a list l equals the sum of counts of a in the P-filtered and non-P-filtered parts of l.

Русский

Для любого предиката P над α счёт числа a в списке l равен сумме счётов a в отфильтрованной P части и не-P части списка.

LaTeX

$$$\\operatorname{count}(a,l) = \\operatorname{count}(a,l.filter P) + \\operatorname{count}(a,l.filter(\\neg P\\,))$$$

Lean4

theorem count_eq_count_filter_add [DecidableEq α] (P : α → Prop) [DecidablePred P] (l : List α) (a : α) :
    count a l = count a (l.filter P) + count a (l.filter (¬P ·)) :=
  by
  convert countP_eq_countP_filter_add l _ P
  simp only [decide_not]

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