finprod_eq_mulIndicator_apply — Mathlib

English

For any set s and function f, the finprod over i with i ∈ s equals the product given by the mulIndicator: ∏ᶠ _ : i ∈ s, f(i) = mulIndicator s f i.

Русский

Для множества s и функции f произведение по i с условием i ∈ s равно mulIndicator s f i.

LaTeX

$$$$ \prod^{\mathrm{fin}}_{i:\, i\in s} f(i) = \operatorname{mulIndicator}(s,f,i). $$$$

Lean4

@[to_additive]
theorem finprod_eq_mulIndicator_apply (s : Set α) (f : α → M) (a : α) : ∏ᶠ _ : a ∈ s, f a = mulIndicator s f a := by
  classical convert finprod_eq_if (M := M) (p := a ∈ s) (x := f a)

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