English
If f: α → M and s ⊆ M are such that s ∩ mulSupport f = t ∩ mulSupport f for some t Finset, then the finprod over s equals the product over t: ∏ᶠ i ∈ s, f i = ∏ i ∈ t, f i.
Русский
Если для f: α → M и подмножества s ∈ Set α выполняется равенство s ∩ mulSupport f = t ∩ mulSupport f, то финпроизводство по s равно произведению по t.
LaTeX
$$$$ \prod^{\mathrm{fin}}_{i \in s} f(i) = \prod_{i \in t} f(i). $$$$
Lean4
@[to_additive]
theorem finprod_mem_eq_prod_of_inter_mulSupport_eq (f : α → M) {s : Set α} {t : Finset α}
(h : s ∩ mulSupport f = t.toSet ∩ mulSupport f) : ∏ᶠ i ∈ s, f i = ∏ i ∈ t, f i :=
finprod_cond_eq_prod_of_cond_iff _ <| by
intro x hxf
rw [← mem_mulSupport] at hxf
refine ⟨fun hx => ?_, fun hx => ?_⟩
· refine ((mem_inter_iff x t (mulSupport f)).mp ?_).1
rw [← Set.ext_iff.mp h x, mem_inter_iff]
exact ⟨hx, hxf⟩
· refine ((mem_inter_iff x s (mulSupport f)).mp ?_).1
rw [Set.ext_iff.mp h x, mem_inter_iff]
exact ⟨hx, hxf⟩
