English
If f is differentiable within s at x and g₁ is differentiable within t' at h x, with h mapping s to t', then g₁ ∘ h is differentiable within s at x with derivative h' · g₁'.
Русский
Если f дифференцируема внутри s в x и g₁ дифференцируема внутри t' в h x, причем h отображает s в t', то g₁ ∘ h дифференцируема внутри s в x с производной h' · g₁'.
LaTeX
$$$\text{If } f: \mathbb{K} \to F \text{ is differentiable within } s \text{ at } x, \text{ and } g_1: \mathbb{K}' \to F \text{ is differentiable within } t' \text{ at } h x, \text{ with } h: 𝕜 \to 𝕜', \text{ and } h s \subset t', \text{ then } (g_1 \circ h) \text{ is differentiable within } s \text{ at } x$ with derivative $h' \cdot g_1'.$$$
Lean4
theorem scomp_hasDerivAt (hg : HasDerivWithinAt g₁ g₁' s' (h x)) (hh : HasDerivAt h h' x) (hs : ∀ x, h x ∈ s') :
HasDerivAt (g₁ ∘ h) (h' • g₁') x :=
hg.scomp x hh <| tendsto_inf.2 ⟨hh.continuousAt, tendsto_principal.2 <| Eventually.of_forall hs⟩
