English
Applying a linear map to a vector is differentiable: if g is differentiable as a map to linear maps and f is differentiable as a vector-valued map, then x ↦ g(x)(f(x)) is differentiable.
Русский
Применение линейного отображения к вектору дифференциируемо: если g дифференцируемо, и f дифференцируемо, то x ↦ g(x)(f(x)) дифференцируемо.
LaTeX
$$$$\text{If } g: M \to F_1 \to_L[𝕜] F_2,\ f: M \to F_1, \, \text{and } g \text{ and } f \text{ are differentiableWithinAt, then } x \mapsto g(x)(f(x)) \text{ is differentiableWithinAt.}$$$$
Lean4
theorem clm_comp {g : M → F₁ →L[𝕜] F₃} {f : M → F₂ →L[𝕜] F₁} {s : Set M}
(hg : MDifferentiableOn I 𝓘(𝕜, F₁ →L[𝕜] F₃) g s) (hf : MDifferentiableOn I 𝓘(𝕜, F₂ →L[𝕜] F₁) f s) :
MDifferentiableOn I 𝓘(𝕜, F₂ →L[𝕜] F₃) (fun x => (g x).comp (f x)) s := fun x hx => (hg x hx).clm_comp (hf x hx)
