no goals
α : Type u_1
β : Type u_2
γ : Type ?u.331376
δ : Type ?u.331379
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
x : α
h : s ∈ 𝓝 x
⊢ ContinuousWithinAt f s x ↔ ContinuousAt f x
rw [← univ_inter s, continuousWithinAt_inter h, continuousWithinAt_univ]