English
If l has a Fréchet derivative l' at f(x) and f has a (classical) derivative f' at x, then the derivative of the composition l ∘ f at x is given by applying l' to the derivative f'.
Русский
Если l имеет предел Фреше дериватив l' в точке f(x), и f имеет производную f' в x, то производная композиции l ∘ f в x равна l'(f(x)) приложенной к f'(x).
LaTeX
$$$$HasDerivWithinAt (l \circ f) (l' f')\ s x \,\;\text{(из предпосылок: }HasFDerivWithinAt l l' t (f x)\text{ и }HasDerivWithinAt f f' s x\text{ и }hst)$$$$
Lean4
/-- The composition `l ∘ f` where `l : F → E` and `f : 𝕜 → F`, has a derivative within a set
equal to the Fréchet derivative of `l` applied to the derivative of `f`. -/
theorem comp_hasDerivWithinAt {t : Set F} (hl : HasFDerivWithinAt l l' t (f x)) (hf : HasDerivWithinAt f f' s x)
(hst : MapsTo f s t) : HasDerivWithinAt (l ∘ f) (l' f') s x := by
simpa only [one_apply, one_smul, smulRight_apply, coe_comp', (· ∘ ·)] using
(hl.comp x hf.hasFDerivWithinAt hst).hasDerivWithinAt
