class PiBase.DieudonneCompleteSpace (X : Type u) [t : TopologicalSpace X] : Prop

• complete_uniformity : ∃ (s : UniformSpace X), s.toTopologicalSpace = t ∧ CompleteSpace X