contMDiffOn_finset_prod — Mathlib

English

If every f_i is ContMDiffOn s for i in t, then the finite product over t is ContMDiffOn s.

Русский

Если каждый f_i является ContMDiffOn на s для i в t, то произведение по t на s дифференцируемо.

LaTeX

$$$\big( \forall i ∈ t, \ ContMDiffOn I' I n (f_i) s \big) \to \ ContMDiffOn I' I n (\prod_{i ∈ t} f_i) s$$

Lean4

@[to_additive]
theorem contMDiffOn_finset_prod (h : ∀ i ∈ t, ContMDiffOn I' I n (f i) s) :
    ContMDiffOn I' I n (fun x => ∏ i ∈ t, f i x) s := fun x hx => contMDiffWithinAt_finset_prod fun i hi => h i hi x hx

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