English
Let f: M → M′ and g: M′ → M″ be differentiable in the MFDeriv sense at x and f(x) respectively, with f(x) = y. Then the derivative of the composition g ∘ f at x is the composition of derivatives: mfderiv I I'' (g ∘ f) x = (mfderiv I' I'' g (f x)).comp (mfderiv I I' f x).
Русский
Пусть f: M → M′ и g: M′ → M″ дифференцируемы в смысле MFDeriv в точке x и в точке f(x) соответственно, и f(x) = y. Тогда производная композиции gi f равна композиции производных: mfderiv I I'' (g ∘ f) x = (mfderiv I' I'' g (f x)).comp (mfderiv I I' f x).
LaTeX
$$$\text{mfderiv } I I'' (g \circ f) x = \big(\text{mfderiv } I' I'' g (f x)\big) .\mathrm{comp}\Big(\text{mfderiv } I I' f x\Big).$$$
Lean4
theorem mfderiv_comp_of_eq {x : M} {y : M'} (hg : MDifferentiableAt I' I'' g y) (hf : MDifferentiableAt I I' f x)
(hy : f x = y) : mfderiv I I'' (g ∘ f) x = (mfderiv I' I'' g (f x)).comp (mfderiv I I' f x) := by subst hy;
exact mfderiv_comp x hg hf
