no goals
α : Type u_1
β : Type u_2
γ : Type ?u.318436
δ : Type ?u.318439
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
a : α
⊢ ContinuousWithinAt f {a} a
simpa only [ContinuousWithinAt, nhdsWithin_singleton, tendsto_pure_left] using fun s =>
  mem_of_mem_nhds