α : Type u_1
β : Type u_2
γ : Type ?u.335557
δ : Type ?u.335560
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
h : ContinuousOn f univ
⊢ ContinuousOn f s
α : Type u_1
β : Type u_2
γ : Type ?u.335557
δ : Type ?u.335560
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
h : Continuous f
⊢ ContinuousOn f s
rw [continuous_iff_continuousOn_univ] at h
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.335557
δ : Type ?u.335560
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
h : ContinuousOn f univ
⊢ ContinuousOn f s
exact h.mono (subset_univ _)