English
Let M be a charted space, and let g: M → L(F1, F3) and f: M → L(F2, F4) be ContMDiffWithinAt of level n on a set s at a point x. Then the map x ↦ (g(x)) prodMap (f(x)) is ContMDiffWithinAt of level n from M to L(F1 × F2, F3 × F4) on the same set and point.
Русский
Пусть M—плоскость/charted space; пусть g: M → L(F1, F3) и f: M → L(F2, F4) гладкие в пределах множества s в точке x. Тогда отображение x ↦ (g(x)) ·prodMap (f(x)) есть гладкость класса ContMDiffWithinAt уровня n от M в L(F1 × F2, F3 × F4) на том же множества s и в той же точке.
LaTeX
$$$\forall \ g:\, M \to \mathcal L_{\mathbb k}(F_1,F_3),\ f:\, M \to \mathcal L_{\mathbb k}(F_2,F_4),\ s \subset M,\ x \in s,\ n\ge 0,\n\; (\hg : \ ContMDiffWithinAt I 𝓘(\mathbb k, F_1 \toL[\mathbb k] F_3) n g s x)\, (hf : \ ContMDiffWithinAt I 𝓘(\mathbb k, F_2 \toL[\mathbb k] F_4) n f s x)\Longrightarrow \\ ContMDiffWithinAt I 𝓘(\mathbb k, F_1 \times F_2 \toL[\mathbb k] F_3 \times F_4) n (\lambda x: (g x).prodMap (f x)) s x$$$
Lean4
theorem clm_prodMap {g : M → F₁ →L[𝕜] F₃} {f : M → F₂ →L[𝕜] F₄} {s : Set M} {x : M}
(hg : ContMDiffWithinAt I 𝓘(𝕜, F₁ →L[𝕜] F₃) n g s x) (hf : ContMDiffWithinAt I 𝓘(𝕜, F₂ →L[𝕜] F₄) n f s x) :
ContMDiffWithinAt I 𝓘(𝕜, F₁ × F₂ →L[𝕜] F₃ × F₄) n (fun x => (g x).prodMap (f x)) s x :=
ContDiff.comp_contMDiffWithinAt (g := fun x : (F₁ →L[𝕜] F₃) × (F₂ →L[𝕜] F₄) => x.1.prodMap x.2) (f := fun x =>
(g x, f x)) (ContinuousLinearMap.prodMapL 𝕜 F₁ F₃ F₂ F₄).contDiff (hg.prodMk_space hf)
