English
If f: M → F1 →L F2 is ContMDiffWithinAt on s, then the map y ↦ (f y).precomp F3 is ContMDiffWithinAt on s.
Русский
Если f гладко на s, то предкомпозиция в F3 гладко на s.
LaTeX
$$$\\forall f:\\, M \\to F_1 \\to_L F_2,\\ ContMDiffWithinAt I 𝓘(𝕜, F_1 \\to_L F_2) n f s x \\Rightarrow ContMDiffWithinAt I 𝓘(𝕜, (F_2 \\to_L F_3) \\to_L (F_1 \\to_L F_3)) n (fun y => (f y).precomp F_3) s x.$$$
Lean4
theorem clm_comp {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₂ →L[𝕜] F₃) n (fun x => (g x).comp (f x)) s x :=
ContDiff.comp_contMDiffWithinAt (g := fun x : (F₁ →L[𝕜] F₃) × (F₂ →L[𝕜] F₁) => x.1.comp x.2) (f := fun x =>
(g x, f x)) (contDiff_fst.clm_comp contDiff_snd) (hg.prodMk_space hf)
