contMDiff_finset_prod — Mathlib

English

If a family f_i is ContMDiffOn with locally finite support, the infinite finite product ∏ᶠ_i f_i is ContMDiffOn.

Русский

Если семейство f_i имеет локально конечную поддержку и каждое f_i континуально-дифференцируемо, то локально сходящееся произведение ContMDiffOn.

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 contMDiff_finset_prod (h : ∀ i ∈ t, ContMDiff I' I n (f i)) : ContMDiff I' I n fun x => ∏ i ∈ t, f i x :=
  fun x => contMDiffAt_finset_prod fun i hi => h i hi x

Похожие утверждения