theorem PiBase.pseudoMetrizableSpace_iff_exists_pseudoMetric (X : Type u) [τ : TopologicalSpace X] : TopologicalSpace.PseudoMetrizableSpace X ↔ ∃ (t : PseudoMetricSpace X), PseudoMetricSpace.toUniformSpace.toTopologicalSpace = τ

theorem PiBase.metrizableSpace_iff_exists_metric (X : Type u) [τ : TopologicalSpace X] : TopologicalSpace.MetrizableSpace X ↔ ∃ (t : MetricSpace X), PseudoMetricSpace.toUniformSpace.toTopologicalSpace = τ

theorem PiBase.WellDefined.pseudoMetrizableSpace : WellDefined TopologicalSpace.PseudoMetrizableSpace