English
If a locally finite family hf yields that mulSupport(f_i) is locally finite, then for each x ∈ X there exists a finite s ⊆ ι such that in a neighborhood of x, the infinite product ∏ᶠ i, f_i y equals the finite product ∏ i∈s, f_i y.
Русский
Для локально конечной семейства hf, задающего локально конечную опору mulSupport(f_i), для каждого x ∈ X существует конечное множество s ⊆ ι, такое что в окрестности x бесконечное произведение ∑ᶠ i, f_i y равно конечному произведению по i ∈ s: ∏ᶠ i, f_i y = ∏ i∈s, f_i y.
LaTeX
$$$\\exists s : \\mathrm{Finset}\\,\\iota,\\; \\forall^\\infty y \\in \\mathcal{N}(x),\\; \\prod^\\! i \\; f_i(y) = \\prod_{i \\in s} f_i(y)$$$
Lean4
@[to_additive]
theorem finprod_eventually_eq_prod {M : Type*} [CommMonoid M] {f : ι → X → M}
(hf : LocallyFinite fun i => mulSupport (f i)) (x : X) :
∃ s : Finset ι, ∀ᶠ y in 𝓝 x, ∏ᶠ i, f i y = ∏ i ∈ s, f i y :=
let ⟨I, hI⟩ := hf.exists_finset_mulSupport x
⟨I, hI.mono fun _ hy => finprod_eq_prod_of_mulSupport_subset _ fun _ hi => hy hi⟩
