filter_pos_add_filter_neg — Mathlib

English

Sum of filtered finsupps equals the filtered sum.

Русский

Сумма фильтрованных финсппов равна фильтрованной сумме.

LaTeX

$$$$ (f.filter p) + (f.filter (\\lambda a. \\lnot p a)) = f. $$$$

Lean4

theorem filter_pos_add_filter_neg [AddZeroClass M] (f : α →₀ M) (p : α → Prop) [DecidablePred p] :
    (f.filter p + f.filter fun a => ¬p a) = f :=
  DFunLike.coe_injective <| by
    simp only [coe_add, filter_eq_indicator]
    exact Set.indicator_self_add_compl {x | p x} f

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