English
If g and f are ContMDiffOn on a set s, then the map x ↦ (g x).prodMap (f x) is ContMDiffOn on s.
Русский
Если обе карты g и f гладкие на множесте s, то отображение x ↦ g(x).prodMap(f(x)) гладко на s.
LaTeX
$$$\forall {s : Set M}, (hg : ContMDiffOn I 𝓘(𝕜, F_1 \toL[𝕜] F_3) n g s) \rightarrow (hf : ContMDiffOn I 𝓘(𝕜, F_2 \toL[𝕜] F_4) n f s) \rightarrow ContMDiffOn I 𝓘(𝕜, F_1 \times F_2 \toL[𝕜] F_3 \times F_4) n (\lambda x: (g x).prodMap (f x)) s$$
Lean4
theorem clm_prodMap {g : M → F₁ →L[𝕜] F₃} {f : M → F₂ →L[𝕜] F₄} {s : Set M} (hg : ContMDiffOn I 𝓘(𝕜, F₁ →L[𝕜] F₃) n g s)
(hf : ContMDiffOn I 𝓘(𝕜, F₂ →L[𝕜] F₄) n f s) :
ContMDiffOn I 𝓘(𝕜, F₁ × F₂ →L[𝕜] F₃ × F₄) n (fun x => (g x).prodMap (f x)) s := fun x hx =>
(hg x hx).clm_prodMap (hf x hx)
