no goals
α : Type u_1
β : Type u_2
γ : Type ?u.340373
δ : Type ?u.340376
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f g : α → β
s : Set α
x : α
h : f =ᶠ[𝓝[s] x] g
hx : f x = g x
⊢ ContinuousWithinAt f s x ↔ ContinuousWithinAt g s x
rw [ContinuousWithinAt, hx, tendsto_congr' h, ContinuousWithinAt]