no goals
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.112160
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
⊢ UniformContinuousOn f univ ↔ UniformContinuous f
rw [UniformContinuousOn, UniformContinuous, univ_prod_univ, principal_univ, inf_top_eq]