no goals
α : Type u
β : Type v
X : Type ?u.127935
ι : Type ?u.127938
inst✝¹ : PseudoMetricSpace α
x y z : α
δ ε ε₁ ε₂ : ℝ
s : Set α
inst✝ : TopologicalSpace β
f : β → α
b : β
⊢ ContinuousAt f b ↔ ∀ (ε : ℝ), ε > 0 → ∀ᶠ (x : β) in 𝓝 b, dist (f x) (f b) < ε
rw [ContinuousAt, tendsto_nhds]