English
Let h₂ be differentiable at f(x) with derivative h₂′, and suppose f has a Fréchet derivative f′ on a set s at x. Then the derivative within s of the composition h₂ ∘ f at x is h₂′ • f′.
Русский
Пусть h₂ дифференцируема в точке f(x) с производной h₂′, и пусть f имеет аппроксимацию Фрéше на множество s в точке x. Тогда внутри множества s производная композиции h₂ ∘ f в x равна h₂′ • f′.
LaTeX
$$$$\\forall f:E\\to 𝕜',\\; f':E\\toL[𝕜] 𝕜',\\; s\\subseteq 𝕜,\\; x:\\;\\text{HasFDerivWithinAt}(f,f',s,x)\\;\\Rightarrow\\; \\text{HasDerivWithinAt}(h_2,h_2',f(x),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} (x) (hh : HasDerivAt h₂ h₂' (f x))
(hf : HasFDerivWithinAt f f' s x) : HasFDerivWithinAt (h₂ ∘ f) (h₂' • f') s x :=
hh.comp_hasFDerivAtFilter x hf hf.continuousWithinAt
