Continuity at isolated points

Stream: Is there code for X?

[Yongxi Lin (Aaron)]

Do we have a theorem similar to the following one?

import Mathlib

open TopologicalSpace Topology

variable {X Y : Type*} (f : X → Y) [TopologicalSpace X] [TopologicalSpace Y] (x : X) (s : Set X)

lemma Continuous_at_isolated_point (h : 𝓝[s \ { x }] x = ⊥) : ContinuousWithinAt f s x := by
  rw [← continuousWithinAt_diff_self]
  unfold ContinuousWithinAt
  simp [h]

I think this is useful and happy to make a PR.

[Aaron Liu]

this should be called something like ContinuousWithinAt.of_isolated

[Yongxi Lin (Aaron)]

Sorry for still not being familiar with Mathlib's naming conventions :smiling_face_with_tear:

[Yongxi Lin (Aaron)]

Are you suggesting that I should change the name of the theorem I posted (when I make a PR) or there is an existing theorem named ContinuousWithinAt.of_isolated?

[Aaron Liu]

I guess both?

[Aaron Liu]

if it exists already that would be great too

[Etienne Marion]

@loogle nhdsWithin, (⊥ : Filter _), "cont"

[loogle]

:shrug: nothing found

[Sébastien Gouëzel]

It's maybe better to phrase it in terms of AccPt as in docs#fderivWithin_zero_of_not_accPt

[Yongxi Lin (Aaron)]

#33065