ContinuousAt iff Tendsto on a punctured nhd

Stream: Is there code for X?

[Geoffrey Irving]

I feel like we have to have this, but I can't find it:

lemma continuousAt_iff_tendsto_nhdsWithin {X Y : Type} [TopologicalSpace X] [TopologicalSpace Y]
    {f : X → Y} {x : X} : ContinuousAt f x ↔ Tendsto f (𝓝[≠] x) (𝓝 (f x)) := by
  constructor
  · exact tendsto_nhdsWithin_of_tendsto_nhds
  · intro h
    simp only [ContinuousAt, ← nhdsWithin_compl_singleton_sup_pure x]
    exact h.sup (tendsto_pure_nhds f x)

[Geoffrey Irving]

To add to the frustration, I seem to remember proving this before myself, but I can't find that either.

[Geoffrey Irving]

Aha, found what I needed: docs#nhdsWithin_compl_singleton_sup_pure.

[Yury G. Kudryashov]

See docs#continuousWithinAt_compl_self