English
If f: M → F1 →L F2 is ContMDiffAt x, then the map y ↦ (f(y)).precomp F3 is ContMDiffAt x in the corresponding target space.
Русский
Если f: M → F1 →L F2 гладко в точке x, то $y \\mapsto (f(y)).precomp F_3$ гладко в той же точке.
LaTeX
$$$\\text{If } f: M \\to F_1 \\to_L F_2 \\text{ is ContMDiffAt } I\\, 𝓘(𝕜,F_1\\to_L F_2)\\, n f x,\\ \\text{then } x \\mapsto (f(x)).precomp F_3\\text{ is ContMDiffAt } I\\, 𝓘(𝕜,(F_2\\to_L F_3)\\to_L(F_1\\to_L F_3))\\, n\\, (f) x.$$$
Lean4
theorem clm_precomp {f : M → F₁ →L[𝕜] F₂} {s : Set M} {x : M} (hf : ContMDiffWithinAt I 𝓘(𝕜, F₁ →L[𝕜] F₂) n f s x) :
ContMDiffWithinAt I 𝓘(𝕜, (F₂ →L[𝕜] F₃) →L[𝕜] (F₁ →L[𝕜] F₃)) n
(fun y ↦ (f y).precomp F₃ : M → (F₂ →L[𝕜] F₃) →L[𝕜] (F₁ →L[𝕜] F₃)) s x :=
ContDiff.comp_contMDiffWithinAt (g := (ContinuousLinearMap.compL 𝕜 F₁ F₂ F₃).flip) (ContinuousLinearMap.contDiff _) hf
