no goals
α : Type u_1
β : Type u_2
γ : Type ?u.311983
δ : Type ?u.311986
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
⊢ ContinuousOn f s ↔ ∀ (x : α), x ∈ s → ∀ (t : Set β), IsOpen t → f x ∈ t → ∃ u, IsOpen u ∧ x ∈ u ∧ u ∩ s ⊆ f ⁻¹' t
simp only [ContinuousOn, ContinuousWithinAt, tendsto_nhds, mem_nhdsWithin]