no goals
α : Type u_1
β : Type u_2
γ : Type ?u.328491
δ : Type ?u.328494
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
inst✝ : DecidableEq α
f : α → β
x : α
y : β
⊢ ContinuousAt (update f x y) x ↔ Tendsto f (𝓝[{x}ᶜ] x) (𝓝 y)
rw [← continuousWithinAt_univ, continuousWithinAt_update_same, compl_eq_univ_diff]