no goals
α : Type u_1
β : Type u_2
γ : Type ?u.319567
δ : Type ?u.319570
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
⊢ Continuous f ↔ ContinuousOn f univ
simp [continuous_iff_continuousAt, ContinuousOn, ContinuousAt, ContinuousWithinAt,
  nhdsWithin_univ]