scomp_hasDerivWithinAt_of_eq — Mathlib

English

If g₁ g₁' is HasDerivWithinAt at h x within s' and h is HasDerivWithinAt at x within s, with hs: h maps s into s', then HasDerivWithinAt (g₁ ∘ h) (h' · g₁') s x.

Русский

Если g₁ g₁' имеют HasDerivWithinAt в h x внутри s' и h имеет HasDerivWithinAt в x внутри s с hs, то HasDerivWithinAt (g₁ ∘ h) (h' · g₁') s x.

LaTeX

$$$\text{If } hg_1 hg_1' \text{ has within-derivative at } h x, \text{ and } hh_\text{ has within-derivative at } x, \text{ with } hs, \text{ then } \text{HasDerivWithinAt } (g_1 \circ h) (h' \cdot g_1') s x.$$$

Lean4

theorem scomp_hasDerivWithinAt_of_eq (hg : HasDerivAt g₁ g₁' y) (hh : HasDerivWithinAt h h' s x) (hy : y = h x) :
    HasDerivWithinAt (g₁ ∘ h) (h' • g₁') s x := by rw [hy] at hg; exact hg.scomp_hasDerivWithinAt x hh

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