no goals
α : Type u_1
β : Type u_2
γ : Type ?u.326677
δ : Type ?u.326680
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
a : α
⊢ ContinuousWithinAt f ({a}ᶜ) a ↔ ContinuousAt f a
rw [compl_eq_univ_diff, continuousWithinAt_diff_self, continuousWithinAt_univ]