∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {x : α}
  [inst_2 : DecidableEq α] {y : β},
  ContinuousAt (Function.update f x y) x ↔ Filter.Tendsto f (nhdsWithin x {x}ᶜ) (nhds y)