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 α
⊢ TendstoLocallyUniformly F f p ↔ ∀ (x : α), Tendsto (fun y => (f y.snd, F y.fst y.snd)) (p ×ˢ 𝓝 x) (𝓤 β)
simp [← tendstoLocallyUniformlyOn_univ, isOpen_univ.tendstoLocallyUniformlyOn_iff_forall_tendsto]