English
Let t be a Finset ι and f_i: E → 𝔸' be ContDiffOn 𝕜 n on a set s. Then the product y ↦ ∏_{i∈t} f_i(y) is ContDiffOn 𝕜 n on s.
Русский
Пусть t — конечное множество индексов, и для каждого i ∈ t функции f_i: E → 𝔸' принадлежат ContDiffOn 𝕜 n на множестве s. Тогда произведение по i ∈ t гладко на s: y ↦ ∏_{i∈t} f_i(y) ∈ ContDiffOn 𝕜 n на s.
LaTeX
$$$\\\\forall t \\\\in \\\\mathrm{Finset} \\\\; ι \\\\; \\\\forall f : ι \\\\to E \\\\to \\\\mathbb{A}' , \\\\left( \\\\forall i \\\\in t, \ ContDiffOn 𝕜 n \\\\left( f i \right) s \right) \\\\Rightarrow \ ContDiffOn \\\\mathbb{K} n \\\\left( \\lambda y, \\\\prod_{i \\\\in t} f i(y) \\\\right) s$$
Lean4
@[fun_prop]
theorem contDiffOn_prod' {t : Finset ι} {f : ι → E → 𝔸'} (h : ∀ i ∈ t, ContDiffOn 𝕜 n (f i) s) :
ContDiffOn 𝕜 n (∏ i ∈ t, f i) s := fun x hx => contDiffWithinAt_prod' fun i hi => h i hi x hx
