English
If h₂ is differentiable at f(x) with derivative h₂′, and f has a Fréchet derivative f′ on s at x, then the composition h₂ ∘ f has a derivative within s at x equal to h₂′ • f′.
Русский
Если h₂ дифференцируема в f(x) с производной h₂′, и f имеет Фрéше-дифференцируемость на s в x, то композиция h₂ ∘ f имеет внутри-дифференциал в x равный h₂′ • f′.
LaTeX
$$$$\\forall x\\, s\\, f\\, f'\\, h_2\\;\\Bigl(\\text{HasDerivAt}(h_2,h_2',f(x))\\Bigr) \\land \\text{HasFDerivWithinAt}(f,f',s,x) \\Rightarrow \\text{HasFDerivWithinAt}(h_2\\circ f,(h_2'\\cdot f'),s,x). $$$$
Lean4
theorem comp_hasFDerivWithinAt {f : E → 𝕜'} {f' : E →L[𝕜] 𝕜'} {s t} (x) (hh : HasDerivWithinAt h₂ h₂' t (f x))
(hf : HasFDerivWithinAt f f' s x) (hst : MapsTo f s t) : HasFDerivWithinAt (h₂ ∘ f) (h₂' • f') s x :=
hh.comp_hasFDerivAtFilter x hf <| hf.continuousWithinAt.tendsto_nhdsWithin hst
