no goals
α : Type u
β : Type v
X : Type ?u.128835
ι : Type ?u.128838
inst✝¹ : PseudoMetricSpace α
x y z : α
δ ε ε₁ ε₂ : ℝ
s✝ : Set α
inst✝ : TopologicalSpace β
f : β → α
s : Set β
⊢ ContinuousOn f s ↔ ∀ (b : β), b ∈ s → ∀ (ε : ℝ), ε > 0 → ∀ᶠ (x : β) in 𝓝[s] b, dist (f x) (f b) < ε
simp [ContinuousOn, continuousWithinAt_iff']