finprod_mem_finset_eq_prod — Mathlib

English

For any f: α → M and a finite index set s represented as a Finset, the finprod over i in s equals the ordinary Finset product ∏ i ∈ s, f(i).

Русский

Пусть f: α → M и s — конечный множество, рассматриваемый как Finset. Тогда \$ \\prod_{i∈s}^f i = \\prod_{i∈s} f(i) \$.

LaTeX

$$$\\displaystyle \\prod\\!\\!\\_i\\in s f(i) = \\prod\\_{i∈s} f(i)$$$

Lean4

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

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