mfderiv_comp_apply_of_eq — Mathlib

English

If f(x) = y, then the chain rule for mfderiv holds with y substituted for f(x): mfderiv I I'' (g ∘ f) x v = (mfderiv I' I'' g y) ((mfderiv I I' f x) v).

Русский

Если f(x) = y, то правило цепной производной сохраняется с y вместо f(x): D(g∘f)(x)[v] = Dg(y)[Df(x)[v]].

LaTeX

$$$\text{mfderiv } I I'' (g \circ f) x \, v = (\text{mfderiv } I' I'' g y) ( (\text{mfderiv } I I' f x) v ),$ где $y = f(x)$.$$

Lean4

theorem mfderiv_comp_apply_of_eq {y : M'} (hg : MDifferentiableAt I' I'' g y) (hf : MDifferentiableAt I I' f x)
    (hy : f x = y) (v : TangentSpace I x) : mfderiv I I'' (g ∘ f) x v = (mfderiv I' I'' g y) ((mfderiv I I' f x) v) :=
  by subst hy; exact mfderiv_comp_apply _ hg hf v

Похожие утверждения