derivWithin_comp_of_eq — Mathlib

English

Let hh₂ be differentiable at h(x) with derivative h₂', and hh be differentiable at x with derivative h', then the derivative of h₂ ∘ h at x is h₂' * h'.

Русский

Пусть hh₂ дифференцируема в h(x) с производной h₂', а hh — в x с производной h', тогда производная h₂ ∘ h в x равна h₂' * h'.

LaTeX

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

Lean4

theorem derivWithin_comp_of_eq (hh₂ : DifferentiableWithinAt 𝕜' h₂ s' y) (hh : DifferentiableWithinAt 𝕜 h s x)
    (hs : MapsTo h s s') (hy : h x = y) : derivWithin (h₂ ∘ h) s x = derivWithin h₂ s' (h x) * derivWithin h s x := by
  subst hy; exact derivWithin_comp x hh₂ hh hs

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