no goals
α : Type u
β : Type v
X : Type ?u.101350
ι : Type ?u.101353
inst✝¹ : PseudoMetricSpace α
x y z : α
δ ε ε₁ ε₂ : ℝ
s✝ : Set α
inst✝ : PseudoMetricSpace β
f : α → β
a : α
s : Set α
⊢ ContinuousWithinAt f s a ↔ ∀ (ε : ℝ), ε > 0 → ∃ δ, δ > 0 ∧ ∀ {x : α}, x ∈ s → dist x a < δ → dist (f x) (f a) < ε
rw [ContinuousWithinAt, tendsto_nhdsWithin_nhds]