English
If each f_i is continuous and the mulSupport of f_i is locally finite, then the map x ↦ ∏ᶠ i, f_i x is continuous.
Русский
Если каждая функция f_i непрерывна и поддержка умножения mulSupport (f_i) локально конечна, то карта x ↦ ∏ᶠ i, f_i(x) непрерывна.
LaTeX
$$$\\text{Continuous}\ \bigl( x \\mapsto \\prod^\\! i\\ f_i(x) \\bigr)$$$
Lean4
@[to_additive]
theorem continuous_finprod {f : ι → X → M} (hc : ∀ i, Continuous (f i)) (hf : LocallyFinite fun i => mulSupport (f i)) :
Continuous fun x => ∏ᶠ i, f i x :=
by
refine continuous_iff_continuousAt.2 fun x => ?_
rcases finprod_eventually_eq_prod hf x with ⟨s, hs⟩
refine ContinuousAt.congr ?_ (EventuallyEq.symm hs)
exact tendsto_finset_prod _ fun i _ => (hc i).continuousAt
