length_eq_length_filter_add — Mathlib

English

For any list l and predicate f, the length of l equals the sum of the lengths of its elements satisfying f and those not satisfying f: |l| = |filter f l| + |filter (not f) l|.

Русский

Для любого списка l и предиката f длина l равна сумме длин списков, удовлетворяющих f, и не удовлетворяющих f: |l| = |filter f l| + |filter ¬f l|.

LaTeX

$$$$|l| = |\\operatorname{filter} f\, l| + |\\operatorname{filter}(\\lambda x. (f x)^{\\mathsf{not}})\\, l|.$$$$

Lean4

theorem length_eq_length_filter_add {l : List (α)} (f : α → Bool) :
    l.length = (l.filter f).length + (l.filter (!f ·)).length := by
  simp_rw [← List.countP_eq_length_filter, l.length_eq_countP_add_countP f, Bool.not_eq_true, Bool.decide_eq_false]

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