mfderivWithin_eq_mfderiv — Mathlib

English

If s has unique differentiability at x and f is differentiable at x, then mfderivWithin equals mfderiv.

Русский

Если в области s в точке x дифференцируемость уникальна и f дифференцируема в x, то mfderivWithin равно mfderiv.

LaTeX

$$$ (hs : UniqueMDiffWithinAt I s x) (h : MDifferentiableAt I I' f x) : mfderivWithin I I' f s x = mfderiv I I' f x $$$

Lean4

theorem mfderivWithin_eq_mfderiv (hs : UniqueMDiffWithinAt I s x) (h : MDifferentiableAt I I' f x) :
    mfderivWithin I I' f s x = mfderiv I I' f x :=
  by
  rw [← mfderivWithin_univ]
  exact mfderivWithin_subset (subset_univ _) hs h.mdifferentiableWithinAt

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