mfderiv_comp_mfderivWithin — Mathlib

English

If f x = y and hg/hf hold as above for g and f, then mfderivWithin equality holds for g∘f with y.

Русский

Если f(x)=y и выполняются необходимые условия для g и f, то равенство MF-производной для g∘f выполняется в y.

LaTeX

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

Lean4

theorem mfderiv_comp_mfderivWithin (hg : MDifferentiableAt I' I'' g (f x)) (hf : MDifferentiableWithinAt I I' f s x)
    (hxs : UniqueMDiffWithinAt I s x) :
    mfderivWithin I I'' (g ∘ f) s x = (mfderiv I' I'' g (f x)).comp (mfderivWithin I I' f s x) :=
  by
  rw [← mfderivWithin_univ]
  exact mfderivWithin_comp _ hg.mdifferentiableWithinAt hf (by simp) hxs

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