English
If hl is a differentiable within l with derivative l' on t at f x, hf is a differentiable within f with derivative f' on s, and t is mapped by f from s, then the derivative within s of l ∘ f is l' applied to f'.
Русский
Если hl — дифференцируем внутри l с производной l' на t в точке f(x), hf — дифференцируем внутри f с производной f' на s, и f(s) ⊂ t, то производная внутри s от l ∘ f равна l' применённому к f'.
LaTeX
$$$$HasFDerivWithinAt l l' t (f x) \land HasDerivWithinAt f f' s x \land Set.MapsTo f s t \Rightarrow HasDerivWithinAt (Function.comp l f) (ContinuousLinearMap.funLike.coe l' f') s x$$$$
Lean4
theorem fderivWithin_comp_derivWithin {t : Set F} (hl : DifferentiableWithinAt 𝕜 l t (f x))
(hf : DifferentiableWithinAt 𝕜 f s x) (hs : MapsTo f s t) :
derivWithin (l ∘ f) s x = (fderivWithin 𝕜 l t (f x) : F → E) (derivWithin f s x) :=
by
by_cases hsx : UniqueDiffWithinAt 𝕜 s x
· exact (hl.hasFDerivWithinAt.comp_hasDerivWithinAt x hf.hasDerivWithinAt hs).derivWithin hsx
· simp [derivWithin_zero_of_not_uniqueDiffWithinAt hsx]
