no goals
α : Type u
β : Type v
X : Type ?u.101995
ι : Type ?u.101998
inst✝¹ : PseudoMetricSpace α
x y z : α
δ ε ε₁ ε₂ : ℝ
s✝ : Set α
inst✝ : PseudoMetricSpace β
f : α → β
s : Set α
⊢ ContinuousOn f s ↔
    ∀ (b : α), b ∈ s → ∀ (ε : ℝ), ε > 0 → ∃ δ, δ > 0 ∧ ∀ (a : α), a ∈ s → dist a b < δ → dist (f a) (f b) < ε
simp [ContinuousOn, continuousWithinAt_iff]