finprod_mem_def — Mathlib

English

For any set s and function f, the finprod over a ∈ s of f(a) equals the finprod over a of mulIndicator s f a.

Русский

Для множества s и функции f: конечное произведение по a ∈ s от f(a) равно конечному произведению по a от mulIndicator s f a.

LaTeX

$$$$ \prod^{\mathrm{fin}}_{a\in s} f(a) = \prod^{\mathrmfin}}_{a} \ mulIndicator(s,f,a). $$$$

Lean4

@[to_additive]
theorem finprod_mem_def (s : Set α) (f : α → M) : ∏ᶠ a ∈ s, f a = ∏ᶠ a, mulIndicator s f a :=
  finprod_congr <| finprod_eq_mulIndicator_apply s f

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