English
If there is an equality y = f(x) and h₂ is differentiable at y with derivative h₂′, while f has a within-set derivative f′ at x, then the derivative within s of h₂ ∘ f at x equals h₂′ • f′.
Русский
Если есть равенство y = f(x) и h₂ дифференцируема в y с производной h₂′, тогда внутри множества s производная h₂ ∘ f в x равна h₂′ • f′.
LaTeX
$$$$\\forall x,f,f',s,y:\\; y=f(x)\\;\\land\\; \\text{HasDerivWithinAt}(h_2,h_2',t,y) \\land \\text{HasFDerivWithinAt}(f,f',s,x) \\Rightarrow \\text{HasFDerivWithinAt}(h_2\\circ f,(h_2'\\cdot f'),s,x). $$$$
Lean4
theorem comp_hasFDerivWithinAt_of_eq {f : E → 𝕜'} {f' : E →L[𝕜] 𝕜'} {s} (x) (hh : HasDerivAt h₂ h₂' y)
(hf : HasFDerivWithinAt f f' s x) (hy : y = f x) : HasFDerivWithinAt (h₂ ∘ f) (h₂' • f') s x := by rw [hy] at hh;
exact hh.comp_hasFDerivWithinAt x hf
