English
If f(x) = y and hy_holds: differentiable within at y and at x with equality hy, then fderivWithin (g ∘ f) s x equals the composition formula.
Русский
Если f(x) = y и выполняются условия внутри и равенство hy, то внутри-дифференцирование композиции равно формуле композиции.
LaTeX
$$$fderivWithin 𝕜 (g\circ f) s x = (fderivWithin 𝕜 g t (f x)).comp (fderivWithin 𝕜 f s x)$$$
Lean4
theorem fderivWithin_comp {g : F → G} {t : Set F} (hg : DifferentiableWithinAt 𝕜 g t (f x))
(hf : DifferentiableWithinAt 𝕜 f s x) (h : MapsTo f s t) (hxs : UniqueDiffWithinAt 𝕜 s x) :
fderivWithin 𝕜 (g ∘ f) s x = (fderivWithin 𝕜 g t (f x)).comp (fderivWithin 𝕜 f s x) :=
(hg.hasFDerivWithinAt.comp x hf.hasFDerivWithinAt h).fderivWithin hxs
