English
If hg is HasDerivAtFilter g₁ g₁' t' y, hh is HasDerivAtFilter h h' x, hy: y = h x, then HasDerivAtFilter (g₁ ∘ h) (h' · g₁') x.
Русский
Если hg HasDerivAtFilter g₁ g₁' t' y, hh HasDerivAtFilter h h' x, hy: y = h x, тогда HasDerivAtFilter (g₁ ∘ h) (h' · g₁') x.
LaTeX
$$$\text{If } hg : HasDerivAtFilter g_1 g_1' t' y \text{ and } hh : HasDerivAtFilter h h' x, \text{ and } hy : y = h x, \text{ then } HasDerivAtFilter (g_1 \circ h) (h' \cdot g_1') x.$$$
Lean4
theorem scomp_of_eq (hg : DifferentiableWithinAt 𝕜' g₁ t' y) (hh : DifferentiableWithinAt 𝕜 h s x) (hs : MapsTo h s t')
(hy : y = h x) : derivWithin (g₁ ∘ h) s x = derivWithin h s x • derivWithin g₁ t' (h x) := by rw [hy] at hg;
exact derivWithin.scomp x hg hh hs
