filter_eq_sum — Mathlib

English

The filtered sum equals the sum of filtered terms via a decomposition into singles.

Русский

Фильтрованная сумма эквивалентна сумме фильтрованных слагаемых через разложение на единичные слагаемые.

LaTeX

$$$$ f.filter p = \\sum i \\in f.support.filter p, singleton i (f i). $$$$

Lean4

theorem filter_eq_sum (p : α → Prop) [DecidablePred p] (f : α →₀ M) :
    f.filter p = ∑ i ∈ f.support.filter p, single i (f i) :=
  (f.filter p).sum_single.symm.trans <|
    Finset.sum_congr rfl fun x hx => by rw [filter_apply_pos _ _ (mem_filter.1 hx).2]

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