fderivWithin — Mathlib

English

If f is differentiable at x, then fderivWithin 𝕜 f s x equals fderiv 𝕜 f x, provided UniqueDiffWithinAt 𝕜 s x.

Русский

Если f дифференцируема в x, тогда внутри-дериватив равен внешнему деривативу: fderivWithin 𝕜 f s x = fderiv 𝕜 f x при условии UniqueDiffWithinAt 𝕜 s x.

LaTeX

$$$\text{DifferentiableAt } 𝕜 f x \Rightarrow fderivWithin 𝕜 f s x = fderiv 𝕜 f x \text{ under } \text{UniqueDiffWithinAt } 𝕜 s x$$$

Lean4

protected theorem fderivWithin (h : DifferentiableAt 𝕜 f x) (hxs : UniqueDiffWithinAt 𝕜 s x) :
    fderivWithin 𝕜 f s x = fderiv 𝕜 f x :=
  h.hasFDerivAt.hasFDerivWithinAt.fderivWithin hxs

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