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 : α), TendstoUniformlyOnFilter F f p (𝓝 x)
simpa [← tendstoLocallyUniformlyOn_univ, ← nhdsWithin_univ] using
  @tendstoLocallyUniformlyOn_iff_filter _ _ _ _ F f univ p _