English
If g is differentiable within u at f(x) and f is differentiable within s at x, and f⁻¹(u) is nhdsWithin x, then g∘f is differentiable within s at x with composed derivative.
Русский
Если g дифференцируема внутри u в f(x), f дифференцируема внутри s в x, и f⁻¹(u) является nhdsWithin x, то g∘f дифференцируема внутри s в x с композиционной производной.
LaTeX
$$$hg\\,HasMFDerivWithinAt I' I'' g u (f x) g' \\land hf\\,HasMFDerivWithinAt I I' f s x f' \\Rightarrow HasMFDerivWithinAt I I'' (g \\circ f) s x (g' \\circ f')$$$
Lean4
theorem mfderivWithin_comp_of_preimage_mem_nhdsWithin_of_eq {y : M'} (hg : MDifferentiableWithinAt I' I'' g u y)
(hf : MDifferentiableWithinAt I I' f s x) (h : f ⁻¹' u ∈ 𝓝[s] x) (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_of_preimage_mem_nhdsWithin _ hg hf h hxs
