English
If hl gives a Fréchet derivative at f(x) and hy: y = f(x), then the derivative of the composition l ∘ f at x is l' f' at that point.
Русский
Если hl задаёт Фреше-дериватив в f(x) и hy: y = f(x), то производная композиции в x равна l' f' в этой точке.
LaTeX
$$$$HasFDerivWithinAt l l' t (f x) \land HasDerivAt f f' x \land MapsTo f s t \Rightarrow HasDerivWithinAt (l \circ f) (l' f') x$$$$
Lean4
/-- The composition `l ∘ f` where `l : F → E` and `f : 𝕜 → F`, has a derivative equal to the
Fréchet derivative of `l` applied to the derivative of `f`. -/
theorem comp_hasDerivAt (hl : HasFDerivAt l l' (f x)) (hf : HasDerivAt f f' x) : HasDerivAt (l ∘ f) (l' f') x :=
hasDerivWithinAt_univ.mp <| hl.comp_hasDerivWithinAt x hf.hasDerivWithinAt
