English
Let E, F, G, H be normed spaces over 𝕜, with s ⊆ E. Suppose c: E → L(G,H) and d: E → L(F,G) are differentiable on s. Then the map y ↦ c(y) ∘ d(y) from E to L(F,H) is differentiable on s.
Русский
Пусть E, F, G, H — нормированные пространства над 𝕜, s ⊆ E. Пусть c: E → L(G,H) и d: E → L(F,G) дифференцируемы на s. Тогда отображение y ↦ c(y) ∘ d(y) из E в L(F,H) дифференцируемо на s.
LaTeX
$$$ \operatorname{DifferentiableOn}_{\mathbb{K}} c\ s \land \operatorname{DifferentiableOn}_{\mathbb{K}} d\ s \Rightarrow \operatorname{DifferentiableOn}_{\mathbb{K}}\bigl( y \mapsto c(y) \circ d(y) \bigr) \ s$$$
Lean4
@[fun_prop]
theorem clm_comp (hc : DifferentiableOn 𝕜 c s) (hd : DifferentiableOn 𝕜 d s) :
DifferentiableOn 𝕜 (fun y => (c y).comp (d y)) s := fun x hx => (hc x hx).clm_comp (hd x hx)
