English
If y = f(x), and h₂ has derivative h₂' at y, and f has Frechet derivative f' at x, then (h₂ ∘ f) has derivative h₂' · f' at x.
Русский
Если y = f(x) и у h₂ есть производная h₂' в y, и у f есть Фрéш-производная f' в x, тогда (h₂ ∘ f) имеет производную h₂' · f' в x.
LaTeX
$$$\text{If } y = f(x) \text{ and } h_2 \text{ has derivative } h_2' \text{ at } y, \text{ and } f \text{ has Frechet derivative } f' \text{ at } x, \text{ then } h_2 \circ f \text{ has derivative } h_2' \cdot f' \text{ at } x.$$$
Lean4
theorem comp_hasFDerivAtFilter {f : E → 𝕜'} {f' : E →L[𝕜] 𝕜'} (x) {L'' : Filter E}
(hh₂ : HasDerivAtFilter h₂ h₂' (f x) L') (hf : HasFDerivAtFilter f f' x L'') (hL : Tendsto f L'' L') :
HasFDerivAtFilter (h₂ ∘ f) (h₂' • f') x L'' :=
by
convert (hh₂.restrictScalars 𝕜).comp x hf hL
ext x
simp [mul_comm]
