English
For f : α → M and s ⊆ α with Finite mulSupport, finprod over s ∩ mulSupport f equals the product over the finite witness; equivalently, finprod_mem_eq_prod_of_inter_mulSupport_eq with the respective hypotheses.
Русский
Для f: α → M и множества s с конечной mulSupport, финпроизводство по s ∩ mulSupport f равно произведению по конечному набору; эквидентно применимо через finprod_mem_eq_prod_of_inter_mulSupport_eq.
LaTeX
$$$$ \prod^{\mathrm{fin}}_{i \in s} f(i) = \prod_{i \in (s \cap \mathrm{mulSupport}(f))} f(i). $$$$
Lean4
@[to_additive]
theorem finprod_mem_eq_prod (f : α → M) {s : Set α} (hf : (s ∩ mulSupport f).Finite) :
∏ᶠ i ∈ s, f i = ∏ i ∈ hf.toFinset, f i :=
finprod_mem_eq_prod_of_inter_mulSupport_eq _ <| by simp [inter_assoc]
