no goals
α : Type u_1
β : Type u_2
γ : Type ?u.305991
δ : Type ?u.305994
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
x : α
⊢ ContinuousWithinAt f univ x ↔ ContinuousAt f x
rw [ContinuousAt, ContinuousWithinAt, nhdsWithin_univ]