deriv_comp_of_eq — 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_of_eq (hh₂ : DifferentiableAt 𝕜' h₂ y) (hh : DifferentiableAt 𝕜 h x) (hy : h x = y) :
    deriv (h₂ ∘ h) x = deriv h₂ (h x) * deriv h x := by subst hy; exact deriv_comp x hh₂ hh

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