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