English
Let f: E → 𝕜′ be differentiable at x with derivative f′, and let h₂: 𝕜′ → 𝕜′ be differentiable at y = f(x) with derivative h₂′. Then the derivative of the composition h₂ ∘ f at x exists and is given by h₂′ • f′.
Русский
Пусть f: E → 𝕜′ дифференцируема в точке x с производной f′, и пусть h₂: 𝕜′ → 𝕜′ дифференцируема в y = f(x) с производной h₂′. Тогда производная композиции h₂ ∘ f в точке x существует и равна h₂′ • f′.
LaTeX
$$$$\\forall f:E\\to 𝕜',\\, f':E\\toL[𝕜] 𝕜',\\, x,\\, y=f(x):\\;\\HasDerivAt(h_2,h_2',y) \\;\\land\\; \\HasFDerivAt(f,f',x)\\;\\Rightarrow\\; \\HasFDerivAt(h_2\\circ f\\, ,\\; h_2'\\cdot f'\\, ,\\; x).$$$$
Lean4
theorem comp_hasFDerivAt_of_eq {f : E → 𝕜'} {f' : E →L[𝕜] 𝕜'} (x) (hh : HasDerivAt h₂ h₂' y) (hf : HasFDerivAt f f' x)
(hy : y = f x) : HasFDerivAt (h₂ ∘ f) (h₂' • f') x := by rw [hy] at hh; exact hh.comp_hasFDerivAt x hf
