English
If hh₂ has derivative h₂' at y and hh has derivative h' at x, and hy: y = h x, and the f-domain matching condition holds, then the derivative within s of h₂ ∘ h at x is h₂' * h'.
Русский
Если у h₂ есть производная в y = h(x) с производной h₂', а у h есть производная в x с производной h', и y = h x, и соблюдается соответствие домена, то внутри s производная h₂ ∘ h в x равна h₂' * h'.
LaTeX
$$$$\\forall x\\; \\text{hh₂: HasDerivWithinAt } h_2 h_2' t y,\; \\text{hh: HasDerivWithinAt } h h' s x,\; \\text{hy: y = h x} \\Rightarrow \\text{HasFDerivWithinAt}(h_2 \\circ h,(h_2' * h'), s, x). $$$$
Lean4
theorem comp_of_eq (hh₂ : HasDerivAtFilter h₂ h₂' y L') (hh : HasDerivAtFilter h h' x L) (hL : Tendsto h L L')
(hy : y = h x) : HasDerivAtFilter (h₂ ∘ h) (h₂' * h') x L := by rw [hy] at hh₂; exact hh₂.comp x hh hL
