fderivWithin — Mathlib

English

If a set supports differentiability around x, then differentiability holds eventually in nhds x.

Русский

Если около x существует область дифференцируемости, то в окрестности x это свойство бесконечно близко к x.

LaTeX

$$$DifferentiableOn\ 𝕜\ f\ s \land s∈ 𝓝 x\Rightarrow \forallᶠ y\ in 𝓝 x, DifferentiableAt\ 𝕜\ f\ y$$$

Lean4

protected theorem fderivWithin (h : HasFDerivWithinAt f f' s x) (hxs : UniqueDiffWithinAt 𝕜 s x) :
    fderivWithin 𝕜 f s x = f' :=
  (hxs.eq h h.differentiableWithinAt.hasFDerivWithinAt).symm

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