prod_filter_index — Mathlib

English

The product of a filtered finsupp equals the product over the filtered support of g.

Русский

Произведение по фильтруемому набору равно произведению по отфильтрованной опоре с функцией g.

LaTeX

$$$$ (f.filter p).prod g = \\prod x \\in (f.filter p).\\mathrm{support},\\; g\\,x\\,(f\\,x). $$$$

Lean4

@[to_additive]
theorem prod_filter_index [CommMonoid N] (g : α → M → N) :
    (f.filter p).prod g = ∏ x ∈ (f.filter p).support, g x (f x) :=
  by
  refine Finset.prod_congr rfl fun x hx => ?_
  rw [support_filter, Finset.mem_filter] at hx
  rw [filter_apply_pos _ _ hx.2]

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