finprod_mem_coe_finset — Mathlib

English

For a function f: α → M and a Finset s, the finprod over (s as a Set) coincides with the Finset product over s.

Русский

Для f: α → M и Finset s произведение по s как множество равно произведению по s как Finset.

LaTeX

$$$\\displaystyle \\left(\\prod\\ᶠ i \\in (s : Set α), f(i)\\right) = \\prod\\_{i∈s} f(i)$$$

Lean4

@[to_additive]
theorem finprod_mem_coe_finset (f : α → M) (s : Finset α) : (∏ᶠ i ∈ (s : Set α), f i) = ∏ i ∈ s, f i :=
  finprod_mem_eq_prod_of_inter_mulSupport_eq _ rfl

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