English
If each f_i is ContMDiffWithinAt and the family has locally finite support, then the infinite product is ContMDiffWithinAt.
Русский
Если для каждого i функция f_i является ContMDiffWithinAt и семейство имеет локально конечную опору, то бесконечное произведение также ContMDiffWithinAt.
LaTeX
$$$\\\\text{LocallyFinite } i \\mapsto mulSupport (f_i) \\\\land \\\\forall i, ContMDiffWithinAt I' I n (f_i) s x \\\\Rightarrow ContMDiffWithinAt I' I n (\\\\lambda x, \\\\prod_i f_i(x)) s x$$$
Lean4
@[to_additive]
theorem contMDiffWithinAt_finprod (lf : LocallyFinite fun i ↦ mulSupport <| f i) {x₀ : M}
(h : ∀ i, ContMDiffWithinAt I' I n (f i) s x₀) : ContMDiffWithinAt I' I n (fun x ↦ ∏ᶠ i, f i x) s x₀ :=
let ⟨_I, hI⟩ := finprod_eventually_eq_prod lf x₀
(ContMDiffWithinAt.prod fun i _hi ↦ h i).congr_of_eventuallyEq (eventually_nhdsWithin_of_eventually_nhds hI)
hI.self_of_nhds
