English
If hh₂ has derivative h₂' at t(y) and hh has derivative h' at s(x), with hy: y = h x, then the derivative within s of h₂ ∘ h at x equals h₂' * h'.
Русский
Если hh₂ имеет производную в t(y) и hh имеет производную в s(x) при hy: y = h x, тогда производная внутри s композиции равна h₂' * h'.
LaTeX
$$$$\\forall x,y\\;\\text{hh₂: HasDerivWithinAt } h_2 h_2' t y\\;\\land\\; \\text{hh: HasDerivWithinAt } h h' s x\\land\\; hy: y=h x \\Rightarrow \\text{HasDerivWithinAt}(h_2\\circ h)(s)(x) (h_2' * h'). $$$$
Lean4
theorem comp (hh₂ : HasDerivWithinAt h₂ h₂' s' (h x)) (hh : HasDerivWithinAt h h' s x) (hst : MapsTo h s s') :
HasDerivWithinAt (h₂ ∘ h) (h₂' * h') s x := by
rw [mul_comm]
exact hh₂.scomp x hh hst
