of_not_accPt — Mathlib

English

If a function is differentiable on a set s and x ∈ s is a limit point of s, then HasFDerivAt f (fderiv 𝕜 f x) x.

Русский

Если f дифференцируема на множестве s и x является точкой внутри 𝓝 x относительно s, то существует производная в точке x.

LaTeX

$$$ \\text{DifferentiableOn } 𝕜 f s \\Rightarrow \\text{DifferentiableAt } 𝕜 f x$ при x ∈ s. $$$

Lean4

/-- If `x` is isolated in `s`, then `f` has any derivative at `x` within `s`,
as this statement is empty. -/
theorem of_not_accPt (h : ¬AccPt x (𝓟 s)) : HasFDerivWithinAt f f' s x :=
  by
  rw [accPt_principal_iff_nhdsWithin, not_neBot] at h
  rw [← hasFDerivWithinAt_diff_singleton x, HasFDerivWithinAt, h, hasFDerivAtFilter_iff_isLittleOTVS]
  exact .bot

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