finprod_mem_eq_finite_toFinset_prod

English

Let f: α → M and hs the hypothesis that s is finite. Then the finprod over i in s equals the product over i in hs.toFinset of f(i).

Русский

Пусть f: α → M и hs: s.Finite. Тогда \$ \\prod_{i∈s} f(i) = \\prod_{i∈hs.toFinset} f(i) \$.

LaTeX

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

Lean4

@[to_additive]
theorem finprod_mem_eq_finite_toFinset_prod (f : α → M) {s : Set α} (hs : s.Finite) :
    ∏ᶠ i ∈ s, f i = ∏ i ∈ hs.toFinset, f i :=
  finprod_mem_eq_prod_of_inter_mulSupport_eq _ <| by rw [hs.coe_toFinset]

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