comp_hasDerivWithinAt — Mathlib

English

Let h be differentiable at x with derivative h′, and let h₂ be differentiable at h(x) with derivative h₂′, and y = h(x). Then the derivative of the composition h₂ ∘ h at x is h₂′ * h′.

Русский

Пусть h дифференцируема в x с производной h′, а h₂ дифференцируема в h(x) с производной h₂′, при этом y = h(x). Тогда производная композиции h₂ ∘ h в x равна h₂′ * h′.

LaTeX

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

Lean4

theorem comp_hasDerivWithinAt (hh₂ : HasDerivAt h₂ h₂' (h x)) (hh : HasDerivWithinAt h h' s x) :
    HasDerivWithinAt (h₂ ∘ h) (h₂' * h') s x :=
  hh₂.hasDerivWithinAt.comp x hh (mapsTo_univ _ _)

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