∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace β] {X : Type u_5} {ιβ : Type u_8} {F : X → α → β} {f : α → β}
  {l : Filter X} {s : Set α} {pβ : ιβ → Prop} {sβ : ιβ → Set (β × β)},
  (uniformity β).HasBasis pβ sβ →
    (TendstoUniformlyOn F f l s ↔ ∀ (i : ιβ), pβ i → ∀ᶠ (n : X) in l, ∀ x ∈ s, (f x, F n x) ∈ sβ i)