English
If hg is HasDerivAtFilter g₁ g₁' at h x with L', and hh is HasDerivAtFilter h h' at x with L, and hL: Tendsto h L L', then HasDerivAtFilter (g₁ ∘ h) (h' · g₁') x.
Русский
Если hg имеет HasDerivAtFilter для g₁ g₁' в h x и hh имеет HasDerivAtFilter для h в x с L, и hL: Tendsto h L L', то HasDerivAtFilter (g₁ ∘ h) (h' · g₁') x.
LaTeX
$$$\text{If } hg : HasDerivAtFilter g_1 g_1' (h x) L', \ hh : HasDerivAtFilter h h' x L, \ hL : Tendsto h L L', \text{ then } HasDerivAtFilter (g_1 \circ h) (h' \cdot g_1') x L.$$$
Lean4
theorem scomp (hg : DifferentiableWithinAt 𝕜' g₁ t' (h x)) (hh : DifferentiableWithinAt 𝕜 h s x) (hs : MapsTo h s t') :
derivWithin (g₁ ∘ h) s x = derivWithin h s x • derivWithin g₁ t' (h x) :=
by
by_cases hsx : UniqueDiffWithinAt 𝕜 s x
· exact (HasDerivWithinAt.scomp x hg.hasDerivWithinAt hh.hasDerivWithinAt hs).derivWithin hsx
· simp [derivWithin_zero_of_not_uniqueDiffWithinAt hsx]
