English
If f x = y and g y is MF-differentiable within u at y, then mfderivWithin I I'' (g ∘ f) s x equals (mfderivWithin I' I'' g u y).comp (mfderivWithin I I' f s x).
Русский
Если f(x)=y и g имеет MF-производную внутри u в y, то mfderivWithin I I'' (g∘f) s x равна композиции mfderivWithin g с mfderivWithin f.
LaTeX
$$$f x = y \\Rightarrow mfderivWithin I I'' (g \\circ f) s x = (mfderivWithin I' I'' g u y).comp (mfderivWithin I I' f s x)$$$
Lean4
theorem mfderivWithin_comp_of_eq {x : M} {y : M'} (hg : MDifferentiableWithinAt I' I'' g u y)
(hf : MDifferentiableWithinAt I I' f s x) (h : s ⊆ f ⁻¹' u) (hxs : UniqueMDiffWithinAt I s x) (hy : f x = y) :
mfderivWithin I I'' (g ∘ f) s x = (mfderivWithin I' I'' g u y).comp (mfderivWithin I I' f s x) := by subst hy;
exact mfderivWithin_comp x hg hf h hxs
