English
If hh₂ has derivative h₂' at y and hh has derivative h' at x, and hy: y = h x, then the derivative within s of h₂ ∘ h at x is h₂' * h'.
Русский
Если hh₂ имеет производную h₂′ в y и hh имеет производную h′ в x, и hy: y = h x, то производная внутри s композиции равна h₂' * h'.
LaTeX
$$$$\\forall x:\\ HasDerivWithinAt h_2 h_2' s' y \\land HasDerivWithinAt h h' s x \\land hy: y = h(x) \\Rightarrow HasDerivWithinAt (h_2\\circ h) (h_2' * h') s x. $$$$
Lean4
theorem derivWithin_comp (hh₂ : DifferentiableWithinAt 𝕜' h₂ s' (h x)) (hh : DifferentiableWithinAt 𝕜 h s x)
(hs : MapsTo h s s') : derivWithin (h₂ ∘ h) s x = derivWithin h₂ s' (h x) * derivWithin h s x :=
by
by_cases hsx : UniqueDiffWithinAt 𝕜 s x
· exact (hh₂.hasDerivWithinAt.comp x hh.hasDerivWithinAt hs).derivWithin hsx
· simp [derivWithin_zero_of_not_uniqueDiffWithinAt hsx]
