no goals
α : Type u
β : Type v
X : Type ?u.33140
inst✝ : PseudoEMetricSpace α
ι : Type u_1
F : ι → β → α
f : β → α
p : Filter ι
⊢ TendstoUniformly F f p ↔ ∀ (ε : ℝ≥0∞), ε > 0 → ∀ᶠ (n : ι) in p, ∀ (x : β), edist (f x) (F n x) < ε
simp only [← tendstoUniformlyOn_univ, tendstoUniformlyOn_iff, mem_univ, forall_const]