English
If a family of linear maps f(y): F1 →L[𝕜] F2 depends differentiably on y in a set s near x, then the map y ↦ f(y) precomposed with a fixed space F3 is differentiable within at s x as a linear map from (F2 →L[𝕜] F3) to (F1 →L[𝕜] F3).
Русский
Если семейство линейных отображений f(y): F1 →L[𝕜] F2 зависит дифференцируемо от y на множества s в окрестности точки x, то отображение y ↦ f(y) ∘ precomp F3 является дифференцируемым внутри на s в точке x как линейное отображение из (F2 →L[𝕜] F3) в (F1 →L[𝕜] F3).
LaTeX
$$$\text{If } f: M \to (F_1 \to_L[\mathbb{K}] F_2) \text{ and } f \text{ is differentiable within at } s \ at \ x, \, then \\ MDifferentiableWithinAt \\ I \, 𝓘(\mathbb{K}, (F_2 \to_L[\mathbb{K}] F_3) \to_L[\mathbb{K}] (F_1 \to_L[\mathbb{K}] F_3)) (y \mapsto (f(y)).precomp F_3) s x. $$$$
Lean4
theorem clm_precomp {f : M → F₁ →L[𝕜] F₂} {s : Set M} {x : M} (hf : MDifferentiableWithinAt I 𝓘(𝕜, F₁ →L[𝕜] F₂) f s x) :
MDifferentiableWithinAt I 𝓘(𝕜, (F₂ →L[𝕜] F₃) →L[𝕜] (F₁ →L[𝕜] F₃))
(fun y ↦ (f y).precomp F₃ : M → (F₂ →L[𝕜] F₃) →L[𝕜] (F₁ →L[𝕜] F₃)) s x :=
Differentiable.comp_mdifferentiableWithinAt
(ContinuousLinearMap.differentiable (ContinuousLinearMap.compL 𝕜 F₁ F₂ F₃).flip) hf
