English
If the family (f_i) indexed by i is locally finite in terms of mulSupport and each f_i is ContMDiffMul, then the locally finite product ∏ᶠ_i f_i is ContMDiffOn on s.
Русский
Если семейство (f_i) локально конечное по поддержке умножения и каждый f_i дифференцируем относительно континуальной структуры на s, то локально конечное произведение ∏ᶠ_i f_i также дифференцируем на s.
LaTeX
$$$\big( \text{LocallyFinite } (\lambda i, \mathrm{mulSupport}(f_i)) \big) \to \Big( \forall i, \ ContMDiffOn I' I n (f_i) s \Big) \to \ ContMDiffOn I' I n \big( \lambda x, \prod^{\text{ᶠ}}_i f_i(x) \big) s$$$
Lean4
@[to_additive]
theorem contMDiffOn_finprod (lf : LocallyFinite fun i ↦ Function.mulSupport <| f i)
(h : ∀ i, ContMDiffOn I' I n (f i) s) : ContMDiffOn I' I n (fun x ↦ ∏ᶠ i, f i x) s := fun x hx ↦
contMDiffWithinAt_finprod lf fun i ↦ h i x hx
