no goals
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : TopologicalSpace α
L : ∀ (u : Set (β × β)), u ∈ 𝓤 β → ∃ F, Continuous F ∧ ∀ (y : α), (f y, F y) ∈ u
⊢ ∀ (u : Set (β × β)), u ∈ 𝓤 β → ∃ F, ContinuousOn F univ ∧ ∀ (y : α), y ∈ univ → (f y, F y) ∈ u
simpa [continuous_iff_continuousOn_univ] using L