tendsto_nhdsNE — Mathlib

English

If f' ≠ 0 at x and f is differentiable there, then f tends to f(x) as we approach x from any punctured neighborhood of x.

Русский

Если f'(x) ≠ 0 и f дифференцируема в окрестности x, то f стремится к f(x) при подходе к x из любой проколотой окрестности x.

LaTeX

$$$ \\mathrm{HasDerivAt} f f' x \\land f' \\neq 0 \\Rightarrow \\mathrm{Tendsto} f (\\mathcal{N}\\setminus\\{x\\}) (\\mathcal{N}\\setminus\\{f(x)\\}) $$$

Lean4

theorem tendsto_nhdsNE (h : HasDerivAt f f' x) (hf' : f' ≠ 0) : Tendsto f (𝓝[≠] x) (𝓝[≠] f x) :=
  tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ h.continuousAt.continuousWithinAt (h.eventually_ne hf')

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