{α : Type u} →
  [inst : TopologicalSpace α] →
    (edist : α → α → ENNReal) →
      (∀ (x : α), edist x x = 0) →
        (∀ (x y : α), edist x y = edist y x) →
          (∀ (x y z : α), edist x z ≤ edist x y + edist y z) →
            (∀ (x : α), (nhds x).HasBasis (fun c => 0 < c) fun c => {y | edist x y < c}) → UniformSpace α