α : Type u_1
β : Type u_2
γ : Type ?u.42243
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set α
f : α → β
hs : IsCompact s
hf : ContinuousOn f s
⊢ UniformContinuous (restrict s f)
α : Type u_1
β : Type u_2
γ : Type ?u.42243
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set α
f : α → β
hs : IsCompact s
hf : ContinuousOn f s
⊢ UniformContinuousOn f s
rw [uniformContinuousOn_iff_restrict]
α : Type u_1
β : Type u_2
γ : Type ?u.42243
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set α
f : α → β
hs : CompactSpace ↑s
hf : ContinuousOn f s
⊢ UniformContinuous (restrict s f)
α : Type u_1
β : Type u_2
γ : Type ?u.42243
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set α
f : α → β
hs : IsCompact s
hf : ContinuousOn f s
⊢ UniformContinuous (restrict s f)
rw [isCompact_iff_compactSpace] at hs
α : Type u_1
β : Type u_2
γ : Type ?u.42243
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set α
f : α → β
hs : CompactSpace ↑s
hf : Continuous (restrict s f)
⊢ UniformContinuous (restrict s f)
α : Type u_1
β : Type u_2
γ : Type ?u.42243
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set α
f : α → β
hs : CompactSpace ↑s
hf : ContinuousOn f s
⊢ UniformContinuous (restrict s f)
rw [continuousOn_iff_continuous_restrict] at hf
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.42243
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set α
f : α → β
hs : CompactSpace ↑s
hf : Continuous (restrict s f)
⊢ UniformContinuous (restrict s f)
exact CompactSpace.uniformContinuous_of_continuous hf