English
Let c: E → L(G,H) and d: E → L(F,G) be differentiable at every point. Then y ↦ c(y) ∘ d(y) is differentiable as a map E → L(F,H).
Русский
Пусть c: E → L(G,H) и d: E → L(F,G) дифференцируемы в каждой точке. Тогда y ↦ c(y) ∘ d(y) — дифференцируемая отображение E → L(F,H).
LaTeX
$$$ \operatorname{Differentiable}_{\mathbb{K}} c \Rightarrow \operatorname{Differentiable}_{\mathbb{K}} d \Rightarrow \operatorname{Differentiable}_{\mathbb{K}}\bigl( y \mapsto c(y) \circ d(y) \bigr)$$$
Lean4
theorem fderiv_clm_comp (hc : DifferentiableAt 𝕜 c x) (hd : DifferentiableAt 𝕜 d x) :
fderiv 𝕜 (fun y => (c y).comp (d y)) x =
(compL 𝕜 F G H (c x)).comp (fderiv 𝕜 d x) + ((compL 𝕜 F G H).flip (d x)).comp (fderiv 𝕜 c x) :=
(hc.hasFDerivAt.clm_comp hd.hasFDerivAt).fderiv
