comp_hasDerivAt_of_eq — Mathlib

English

If hh₂ has derivative h₂' at y and hh has derivative h' at x, and 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 comp_hasDerivAt_of_eq {t} (hh₂ : HasDerivWithinAt h₂ h₂' t y) (hh : HasDerivAt h h' x)
    (ht : ∀ᶠ x' in 𝓝 x, h x' ∈ t) (hy : y = h x) : HasDerivAt (h₂ ∘ h) (h₂' * h') x := by subst y;
  exact hh₂.comp_hasDerivAt x hh ht

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