English
If hh₂ is HasDerivAtFilter at h(x) with derivative h₂', and hh is HasDerivAtFilter at x with derivative h', then the composition h₂ ∘ h has HasDerivAtFilter at x with derivative h₂' * h'.
Русский
Если hh₂ имеет производную в h(x) с производной h₂', и hh имеет производную в x с производной h', то композиция h₂ ∘ h имеет производную по фильтру в x равную h₂' * h'.
LaTeX
$$$$\\forall x:\\ HasDerivAtFilter h₂ h₂' (h x) \\to HasDerivAtFilter h h' x \\to HasDerivAtFilter (h₂ \\circ h) (h₂' * h') x. $$$$
Lean4
theorem comp (hh₂ : HasDerivAtFilter h₂ h₂' (h x) L') (hh : HasDerivAtFilter h h' x L) (hL : Tendsto h L L') :
HasDerivAtFilter (h₂ ∘ h) (h₂' * h') x L := by
rw [mul_comm]
exact hh₂.scomp x hh hL
