English
If a map y ↦ f(y) is differentiable in the sense of linear maps from F2 to F3, then the postcomposition with a fixed F1 →L F2 yields a differentiable map y ↦ f(y).postcomp F1 from (F1 →L F2) to (F1 →L F3).
Русский
Если отображение y ↦ f(y) дифференцируемо как линейное отображение F2 → F3, то посткомпоновка с фиксированным F1 → L F2 даёт дифференцируемое отображение y ↦ f(y).postcomp F1 от (F1 →L F2) к (F1 →L F3).
LaTeX
$$$$\text{If } f: M \to F_2 \to_L F_3 \text{ is differentiable withinAt, then } (\lambda y. (f(y)).postcomp F_1): M \to (F_1 \to_L F_2) \to_L (F_1 \to_L F_3) \text{ is differentiable withinAt.}$$$$
Lean4
theorem clm_postcomp {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).postcomp F₁ : M → (F₁ →L[𝕜] F₂) →L[𝕜] (F₁ →L[𝕜] F₃)) s x :=
Differentiable.comp_mdifferentiableWithinAt
(ContinuousLinearMap.differentiable (ContinuousLinearMap.compL 𝕜 F₁ F₂ F₃)) hf
