English
For any tangent vector v at x, the derivative of the composition applied to v is the derivative of g at f(x) applied to the derivative of f at x applied to v: mfderiv I I'' (g ∘ f) x v = (mfderiv I' I'' g (f x)) ((mfderiv I I' f x) v).
Русский
Для любого вектора касательной v в точке x производная композиции, применённая к v, равна применению производной g в точке f(x) к производной f в x на v: D(g∘f)(x)[v] = Dg(f(x))[Df(x)[v]].
LaTeX
$$$\text{mfderiv } I I'' (g \circ f) x \; v = (\text{mfderiv } I' I'' g (f x)) ( (\text{mfderiv } I I' f x) v ).$$$
Lean4
theorem mfderiv_comp_apply (hg : MDifferentiableAt I' I'' g (f x)) (hf : MDifferentiableAt I I' f x)
(v : TangentSpace I x) : mfderiv I I'' (g ∘ f) x v = (mfderiv I' I'' g (f x)) ((mfderiv I I' f x) v) :=
by
rw [mfderiv_comp _ hg hf]
rfl
