of_nhdsWithin_eq_bot — Mathlib

English

If x is not an accumulation point of s, then f is differentiable within s at x for any derivative.

Русский

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

LaTeX

$$$ \\text{Not }(AccPt x (𝓟 s)) \\Rightarrow HasFDerivWithinAt f f' s x$$$

Lean4

/-- If `x` is isolated in `s`, then `f` has any derivative at `x` within `s`,
as this statement is empty. -/
@[deprecated HasFDerivWithinAt.of_not_accPt (since := "2025-04-20")]
theorem of_nhdsWithin_eq_bot (h : 𝓝[s \ { x }] x = ⊥) : HasFDerivWithinAt f f' s x :=
  .of_not_accPt <| by rwa [accPt_principal_iff_nhdsWithin, not_neBot]

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