English
If f x = y and g y is MDifferentiableWithinAt, then g∘f is MDifferentiableWithinAt with the derivative equal to the derivative of g composed with the derivative of f.
Русский
Если f(x)=y и g(y) дифференцируема внутри, то g∘f дифференцируема внутри и её производная есть композиция производных.
LaTeX
$$$f x = y \\Rightarrow MDifferentiableWithinAt I' I'' g u y \\Rightarrow MDifferentiableWithinAt I I' f s x \\Rightarrow MDifferentiableWithinAt I I'' (g \\circ f) s x$$$
Lean4
theorem mfderivWithin_comp (hg : MDifferentiableWithinAt I' I'' g u (f x)) (hf : MDifferentiableWithinAt I I' f s x)
(h : s ⊆ f ⁻¹' u) (hxs : UniqueMDiffWithinAt I s x) :
mfderivWithin I I'' (g ∘ f) s x = (mfderivWithin I' I'' g u (f x)).comp (mfderivWithin I I' f s x) :=
by
apply HasMFDerivWithinAt.mfderivWithin _ hxs
exact HasMFDerivWithinAt.comp x hg.hasMFDerivWithinAt hf.hasMFDerivWithinAt h
