English
Let f: E → 𝕜′ be differentiable at x with derivative f′, and let h₂: 𝕜′ → 𝕜′ be differentiable at y = f(x) with derivative h₂′. If the image of a neighborhood of x under f lies in a set t, then the derivative of h₂ ∘ f at x is h₂′ • f′.
Русский
Пусть f: E → 𝕜′ дифференцируема в x с производной f′, и пусть h₂: 𝕜′ → 𝕜′ дифференцируема в y=f(x) с производной h₂′. Если окрестность x образуется в t под f, то производная h₂ ∘ f в x равна h₂′ • f′.
LaTeX
$$$$\\forall x, f, f', t, y:\\; y=f(x) \\land \\text{HasDerivAt}(h_2,h_2',y) \\land \\text{HasFDerivAt}(f,f',x) \\land (\\forall x'\\to x: f x' \\in t) \\Rightarrow \\text{HasFDerivAt}(h_2\\circ f,(h_2'\\cdot f'),x). $$$$
Lean4
theorem comp_hasFDerivWithinAt_of_eq {f : E → 𝕜'} {f' : E →L[𝕜] 𝕜'} {s t} (x) (hh : HasDerivWithinAt h₂ h₂' t y)
(hf : HasFDerivWithinAt f f' s x) (hst : MapsTo f s t) (hy : y = f x) : HasFDerivWithinAt (h₂ ∘ f) (h₂' • f') s x :=
by rw [hy] at hh; exact hh.comp_hasFDerivWithinAt x hf hst
