contMDiffOn_finset_prod' — Mathlib

English

If every f_i is ContMDiffOn s for i in t, then the product over t, x ↦ ∏ i∈t f_i(x), is ContMDiffOn s.

Русский

Если для каждого i в t отображение f_i является ContMDiffOn на s, то произведение по t, x ↦ ∏ i∈t f_i(x), также ContMDiffOn на s.

LaTeX

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

Lean4

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

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