no goals
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : T1Space α
inst✝¹ : DecidableEq α
inst✝ : TopologicalSpace β
f : α → β
x y : α
z : β
hne : y ≠ x
⊢ ContinuousAt (update f x z) y ↔ ContinuousAt f y
simp only [← continuousWithinAt_univ, continuousWithinAt_update_of_ne hne]