continuousAt_iff_punctured_nhds — Mathlib

English

Continuity at a is equivalent to convergence along punctured neighborhoods of a.

Русский

Непрерывность в точке a эквивалентна сходимости вдоль пунктированной окрестности a.

LaTeX

$$$$ ContinuousAt(f,a) \\iff Tendsto(f, 𝓝_{\\neq} a, 𝓝(f(a))) $$$$

Lean4

theorem continuousAt_iff_punctured_nhds [TopologicalSpace β] {f : α → β} {a : α} :
    ContinuousAt f a ↔ Tendsto f (𝓝[≠] a) (𝓝 (f a)) := by
  simp [ContinuousAt, -pure_sup_nhdsNE, ← pure_sup_nhdsNE a, tendsto_pure_nhds]

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