English
If each f_i: E → 𝔸' is ContDiff 𝕜 n at x for i in t, then the product is ContDiff 𝕜 n at x.
Русский
Если каждая функция f_i: E → 𝔸' для i в t является ContDiff 𝕜 n в x, то их произведение тоже ContDiff 𝕜 n в x.
LaTeX
$$$\\\\forall t \\\\in \\\\mathrm{Finset} \\\\; ι \\\\; \\\\forall f : ι \\\\to E \\\\to \\\\mathbb{A}', \\\\left( \\\\forall i \\\\in t, \ ContDiff 𝕜 n \\\\left( f i \right) x \right) \\\\Rightarrow \ ContDiff 𝕜 n \\\\left( \\lambda y, \\\\prod_{i \\\\in t} f i(y) \\\\right) x$$
Lean4
@[fun_prop]
theorem contDiffOn_prod {t : Finset ι} {f : ι → E → 𝔸'} (h : ∀ i ∈ t, ContDiffOn 𝕜 n (f i) s) :
ContDiffOn 𝕜 n (fun y => ∏ i ∈ t, f i y) s := fun x hx => contDiffWithinAt_prod fun i hi => h i hi x hx
