mfderivWithin — Mathlib

English

The mfderivWithin equals mfderiv when the hypothesis guarantees unique differentiability within the set.

Русский

mfderivWithin равен mfderiv при условии уникальности дифференцируемости внутри множества.

LaTeX

$$$ (h : MDifferentiableWithinAt I I' f s x) (hxs : UniqueMDiffWithinAt I s x) : mfderivWithin I I' f s x = mfderiv I I' f x $$$

Lean4

protected theorem mfderivWithin (h : HasMFDerivWithinAt I I' f s x f') (hxs : UniqueMDiffWithinAt I s x) :
    mfderivWithin I I' f s x = f' := by
  ext
  rw [hxs.eq h h.mdifferentiableWithinAt.hasMFDerivWithinAt]

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