no goals
α : Type u
β : Type v
X : Type ?u.31390
inst✝¹ : PseudoEMetricSpace α
ι : Type u_1
inst✝ : TopologicalSpace β
F : ι → β → α
f : β → α
p : Filter ι
⊢ TendstoLocallyUniformly F f p ↔
    ∀ (ε : ℝ≥0∞), ε > 0 → ∀ (x : β), ∃ t, t ∈ 𝓝 x ∧ ∀ᶠ (n : ι) in p, ∀ (y : β), y ∈ t → edist (f y) (F n y) < ε
simp only [← tendstoLocallyUniformlyOn_univ, tendstoLocallyUniformlyOn_iff, mem_univ,
  forall_const, exists_prop, nhdsWithin_univ]