no goals
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f✝ : α → β
s s' : Set α
x✝ : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝¹ : UniformSpace α
inst✝ : UniformSpace γ
f : α → β → γ
h : UniformContinuous₂ f
x : α
⊢ UniformContinuousOn (↿f) (univ ×ˢ univ)
rwa [univ_prod_univ, uniformContinuousOn_univ]