finprod_mem_eq_toFinset_prod — Mathlib

English

Let f: α → M and a subset s of α with s finite. Then the finite product over i in s of f(i) equals the product over i in s.toFinset of f(i).

Русский

Пусть f: α → M и s ⊆ α таково, что s конечно. Тогда конечный произведение по i∈s f(i) равно произведению по i∈s.toFinset f(i).

LaTeX

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

Lean4

@[to_additive]
theorem finprod_mem_eq_toFinset_prod (f : α → M) (s : Set α) [Fintype s] : ∏ᶠ i ∈ s, f i = ∏ i ∈ s.toFinset, f i :=
  finprod_mem_eq_prod_of_inter_mulSupport_eq _ <| by simp_rw [coe_toFinset s]

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