mfderivWithin — Mathlib

English

If MDifferentiableAt I I' f x, then HasMFDerivAt I I' f x (mfderiv I I' f x).

Русский

Если функция дифференцируема в точке x, то существует MF-производная в x равная mfderiv I I' f x.

LaTeX

$$$ (h : MDifferentiableAt I I' f x) : HasMFDerivAt I I' f x (mfderiv I I' f x) $$$

Lean4

theorem mfderivWithin (h : MDifferentiableAt I I' f x) (hxs : UniqueMDiffWithinAt I s x) :
    mfderivWithin I I' f s x = mfderiv I I' f x :=
  by
  apply HasMFDerivWithinAt.mfderivWithin _ hxs
  exact h.hasMFDerivAt.hasMFDerivWithinAt

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