English
If hg and hf assert ContMDiffAt at a point x for g and f respectively, then the function x ↦ (g x).prodMap (f x) is ContMDiffAt at x for the product space of their targets.
Русский
Если hg и hf дают ContMDiffAt в точке x для функций g и f соответственно, то x ↦ (g x).prodMap (f x) является ContMDiffAt в точке x для произведенного пространства целей.
LaTeX
$$$\forall {\, 𝕜, E, F_1, F_2, F_3, F_4} \quad (hg : ContMDiffAt I 𝓘(𝕜, F_1 \toL[𝕜] F_3) n g x) \land (hf : ContMDiffAt I 𝓘(𝕜, F_2 \toL[𝕜] F_4) n f x) \Rightarrow \\ ContMDiffAt I 𝓘(𝕜, F_1 \times F_2 \toL[𝕜] F_3 \times F_4) n (\lambda x: (g x).prodMap (f x)) x$$
Lean4
nonrec theorem clm_prodMap {g : M → F₁ →L[𝕜] F₃} {f : M → F₂ →L[𝕜] F₄} {x : M}
(hg : ContMDiffAt I 𝓘(𝕜, F₁ →L[𝕜] F₃) n g x) (hf : ContMDiffAt I 𝓘(𝕜, F₂ →L[𝕜] F₄) n f x) :
ContMDiffAt I 𝓘(𝕜, F₁ × F₂ →L[𝕜] F₃ × F₄) n (fun x => (g x).prodMap (f x)) x :=
hg.clm_prodMap hf
