finprod_eq_finset_prod_of_mulSupport_subset

English

For f : α → M, [Equivalences], if hf : (mulSupport f).Finite, then finprod over i with i ∈ s equals s.finset product:

Русский

Для функции f: α → M и конечного множества hf, финпроизводство по i ∈ s равно произведению по i ∈ s.

LaTeX

$$$$ \prod^{\mathrm{fin}}_{i} f(i) = \prod_{i \in s} f(i). $$$$

Lean4

@[to_additive]
theorem finprod_eq_finset_prod_of_mulSupport_subset (f : α → M) {s : Finset α} (h : mulSupport f ⊆ (s : Set α)) :
    ∏ᶠ i, f i = ∏ i ∈ s, f i :=
  haveI h' : (s.finite_toSet.subset h).toFinset ⊆ s := by simpa [← Finset.coe_subset, Set.coe_toFinset]
  finprod_eq_prod_of_mulSupport_toFinset_subset _ _ h'

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