English
If y = f(x), and h₂ is differentiable at y with derivative h₂′, while f is differentiable at x with derivative f′, then the derivative of h₂ ∘ f at x is h₂′ • f′.
Русский
Если y = f(x), и h₂ дифференцируема в y с производной h₂′, а f дифференцируема в x с производной f′, то производная h₂ ∘ f в x равна h₂′ • f′.
LaTeX
$$$$\\forall x, f, f', y:\\; y=f(x) \\land \\text{HasDerivAt}(h_2,h_2',y) \\land \\text{HasFDerivAt}(f,f',x) \\Rightarrow \\text{HasFDerivAt}(h_2\\circ f,(h_2'\\cdot f'),x). $$$$
Lean4
theorem comp_hasFDerivAt {f : E → 𝕜'} {f' : E →L[𝕜] 𝕜'} {t} (x) (hh : HasDerivWithinAt h₂ h₂' t (f x))
(hf : HasFDerivAt f f' x) (ht : ∀ᶠ x' in 𝓝 x, f x' ∈ t) : HasFDerivAt (h₂ ∘ f) (h₂' • f') x :=
hh.comp_hasFDerivAtFilter x hf <| tendsto_nhdsWithin_iff.mpr ⟨hf.continuousAt, ht⟩
