no goals
α : Type u
β : Type v
X : Type ?u.81094
ι✝ : Type ?u.81097
inst✝¹ : PseudoMetricSpace α
x y z : α
δ ε ε₁ ε₂ : ℝ
s : Set α
ι : Type u_1
inst✝ : TopologicalSpace β
F : ι → β → α
f : β → α
p : Filter ι
⊢ TendstoLocallyUniformly F f p ↔
    ∀ (ε : ℝ), ε > 0 → ∀ (x : β), ∃ t, t ∈ 𝓝 x ∧ ∀ᶠ (n : ι) in p, ∀ (y : β), y ∈ t → dist (f y) (F n y) < ε
simp only [← tendstoLocallyUniformlyOn_univ, tendstoLocallyUniformlyOn_iff, nhdsWithin_univ,
  mem_univ, forall_const, exists_prop]