∀ {α : Type u_1} {G : Type u_2} [inst : AddGroup G] [inst_1 : UniformSpace G] [IsUniformAddGroup G] (𝔖 : Set (Set α)),
  𝔖.Nonempty →
    DirectedOn (fun x1 x2 => x1 ⊆ x2) 𝔖 →
      (nhds 0).HasBasis (fun SV => SV.1 ∈ 𝔖 ∧ SV.2 ∈ nhds 0) fun SV => {f | ∀ x ∈ SV.1, f x ∈ SV.2}