filter_pos_add_filter_neg — Mathlib

English

The sum of the p-filter and the not-p-filter equals the original function: f.filter p + f.filter not p = f.

Русский

Сумма фильтров p и не-p равна исходной функции: f.filter p + f.filter not p = f.

LaTeX

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

Lean4

theorem filter_pos_add_filter_neg [∀ i, AddZeroClass (β i)] (f : Π₀ i, β i) (p : ι → Prop) [DecidablePred p] :
    (f.filter p + f.filter fun i => ¬p i) = f :=
  ext fun i => by simp only [add_apply, filter_apply]; split_ifs <;> simp only [add_zero, zero_add]

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