mfderiv_comp_mfderivWithin_of_eq — Mathlib

English

If f(x)=y and g is MF-differentiable at y, then mfderivWithin I I'' (g ∘ f) s x equals (mfderiv I' I'' g y).comp (mfderivWithin I I' f s x).

Русский

Если f(x)=y и g имеет MF-производную в y, то mfderivWithin... равна композиции.

LaTeX

$$$f x = y \\Rightarrow mfderivWithin I I'' (g \\circ f) s x = (mfderiv I' I'' g y).comp (mfderivWithin I I' f s x)$$$

Lean4

theorem mfderiv_comp_mfderivWithin_of_eq {x : M} {y : M'} (hg : MDifferentiableAt I' I'' g y)
    (hf : MDifferentiableWithinAt I I' f s x) (hxs : UniqueMDiffWithinAt I s x) (hy : f x = y) :
    mfderivWithin I I'' (g ∘ f) s x = (mfderiv I' I'' g y).comp (mfderivWithin I I' f s x) := by subst hy;
  exact mfderiv_comp_mfderivWithin x hg hf hxs

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