English
If hl differentiableWithinAt l at y with hy = f x and hf differentiableWithinAt f at x with hs and hy, then the derivative within s of l ∘ f equals the application of fderivWithin to f' times derivWithin f.
Русский
Если l дифференцируем внутри l в y и y = f(x) и f дифференцируем внутри f в x, то производная внутри s от l ∘ f равна fderivWithin(l)(f x) применённой к derivWithin f.
LaTeX
$$$$fderivWithin\ 𝕜 l t (f x) \land DifferentiableWithinAt 𝕜 f s x \Rightarrow derivWithin (l \circ f) s x = (fderivWithin 𝕜 l t (f x) : F \to E) (derivWithin f s x)$$$$
Lean4
theorem fderivWithin_comp_derivWithin_of_eq {t : Set F} (hl : DifferentiableWithinAt 𝕜 l t y)
(hf : DifferentiableWithinAt 𝕜 f s x) (hs : MapsTo f s t) (hy : y = f x) :
derivWithin (l ∘ f) s x = (fderivWithin 𝕜 l t (f x) : F → E) (derivWithin f s x) := by rw [hy] at hl;
exact fderivWithin_comp_derivWithin x hl hf hs
