English
If g₁ is differentiable within t' at y and h is differentiable within s at x with maps h: s → t', then g₁ ∘ h is differentiable within s at x with derivative h' · g₁'.
Русский
Если g₁ дифференцируема внутри t' в y и h дифференцируема внутри s в x, причем h отображает s в t', то g₁ ∘ h дифференцируема внутри s в x с производной h' · g₁'.
LaTeX
$$$\text{If } g_1 \text{ is differentiable within } t' \text{ at } y, \text{ and } h \text{ is differentiable within } s \text{ at } x, \text{ with } h(s) \subset t', \text{ then } g_1 \circ h \text{ is differentiable within } s \text{ at } x \text{ with derivative } h' \cdot g_1'.}$$$
Lean4
theorem scomp_hasDerivWithinAt (hg : HasDerivAt g₁ g₁' (h x)) (hh : HasDerivWithinAt h h' s x) :
HasDerivWithinAt (g₁ ∘ h) (h' • g₁') s x :=
HasDerivWithinAt.scomp x hg.hasDerivWithinAt hh (mapsTo_univ _ _)
