no goals
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.202052
inst✝¹ : UniformSpace α
inst✝ : TopologicalSpace β
f : β → α
s : Set β
⊢ ContinuousOn f s ↔ ∀ (b : β), b ∈ s → Tendsto (fun x => (f x, f b)) (𝓝[s] b) (𝓤 α)
simp [ContinuousOn, continuousWithinAt_iff'_left]