α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.150229
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
h : UniformContinuous (restrict s f)
⊢ ContinuousOn f s
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.150229
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
h : UniformContinuousOn f s
⊢ ContinuousOn f s
rw [uniformContinuousOn_iff_restrict] at h
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.150229
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
h : UniformContinuous (restrict s f)
⊢ Continuous (restrict s f)
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.150229
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
h : UniformContinuous (restrict s f)
⊢ ContinuousOn f s
rw [continuousOn_iff_continuous_restrict]
no goals
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.150229
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
h : UniformContinuous (restrict s f)
⊢ Continuous (restrict s f)
exact h.continuous