finprod_eq_prod_of_mulSupport_toFinset_subset

English

Let f : α → M and hf : (mulSupport f).Finite. Then for any Finset s with hf.toFinset ⊆ s, ∏ᶠ i, f i = ∏ i ∈ s, f i.

Русский

Пусть mulSupport f конечен; тогда если Finset s содержит hf.toFinset, то ∏ᶠ i, f i = ∏ i ∈ s, f i.

LaTeX

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

Lean4

@[to_additive]
theorem finprod_eq_prod_of_mulSupport_toFinset_subset (f : α → M) (hf : (mulSupport f).Finite) {s : Finset α}
    (h : hf.toFinset ⊆ s) : ∏ᶠ i, f i = ∏ i ∈ s, f i :=
  finprod_eq_prod_of_mulSupport_subset _ fun _ hx => h <| hf.mem_toFinset.2 hx

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