English
If hh₂ is HasDerivWithinAt at f x with derivative h₂', and hf is HasFDerivWithinAt at x with derivative f', and MapsTo f s t, then the composition h₂ ∘ f has a HasFDerivWithinAt on s with derivative h₂' • f'.
Русский
Если hh₂ имеет HasDerivWithinAt по f x с производной h₂', и hf имеет HasFDerivWithinAt на s в x с производной f', и f сминает область s в t, тогда композиция имеет HasFDerivWithinAt на s с производной h₂' • f'.
LaTeX
$$$$\\forall x:\\ HasDerivWithinAt h_2 h_2' (f x) \\land HasFDerivWithinAt f f' s x \\Rightarrow HasFDerivWithinAt (h_2\\circ f) (h_2'\\cdot f') s x. $$$$
Lean4
theorem comp_hasDerivWithinAt_of_eq (hh₂ : HasDerivAt h₂ h₂' y) (hh : HasDerivWithinAt h h' s x) (hy : y = h x) :
HasDerivWithinAt (h₂ ∘ h) (h₂' * h') s x := by rw [hy] at hh₂; exact hh₂.comp_hasDerivWithinAt x hh
