English
If l is differentiable within t with derivative l' and f is differentiable within s with derivative f', then the derivative within s of l ∘ f at x equals l' applied to the derivative of f.
Русский
Если l дифференцируем внутри t с производной l' и f дифференцируем внутри s с производной f', то внутри s производная композиции равна применению l' к Deriv(f).
LaTeX
$$$$fderivWithin\ Within (l \circ f) s x = (fderivWithin 𝕜 l t (f x) : F → E) (derivWithin f s x)$$$$
Lean4
/-- The composition `l ∘ f` where `l : F → E` and `f : 𝕜 → F`, has a derivative equal to the
Fréchet derivative of `l` applied to the derivative of `f`. -/
theorem comp_hasDerivAt_of_eq (hl : HasFDerivAt l l' y) (hf : HasDerivAt f f' x) (hy : y = f x) :
HasDerivAt (l ∘ f) (l' f') x := by rw [hy] at hl; exact hl.comp_hasDerivAt x hf
