∀ (α : Type u_1) (β : Type u_2) {ι : Type u_4} [inst : UniformSpace β] (𝔖 : Set (Set α)),
  𝔖.Nonempty →
    DirectedOn (fun x1 x2 => x1 ⊆ x2) 𝔖 →
      ∀ {p : ι → Prop} {s : ι → Set (β × β)},
        (uniformity β).HasBasis p s →
          (uniformity (UniformOnFun α β 𝔖)).HasBasis (fun Si => Si.1 ∈ 𝔖 ∧ p Si.2) fun Si =>
            UniformOnFun.gen 𝔖 Si.1 (s Si.2)