deriv_comp — Mathlib

English

If hh₂ has derivative h₂' at y and hh has derivative h' at x, with y = h x, then the derivative of h₂ ∘ h at x is h₂' * h'.

Русский

Если hh₂ имеет производную h₂′ в y и hh имеет производную h′ в x при y = h x, то производная h₂ ∘ h в x равна h₂' * h'.

LaTeX

$$$$\\forall x:\\ HasDerivAt h₂ h₂' y \\land HasDerivAt h h' x \\land y = h(x) \\Rightarrow HasDerivAt (h_2\\circ h) (h_2' * h') x. $$$$

Lean4

theorem deriv_comp (hh₂ : DifferentiableAt 𝕜' h₂ (h x)) (hh : DifferentiableAt 𝕜 h x) :
    deriv (h₂ ∘ h) x = deriv h₂ (h x) * deriv h x :=
  (hh₂.hasDerivAt.comp x hh.hasDerivAt).deriv

Похожие утверждения