theorem PiBase.Homeomorph.isCompletelyMetrizableSpace {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [h : TopologicalSpace.IsCompletelyMetrizableSpace X] (f : X ≃ₜ Y) : TopologicalSpace.IsCompletelyMetrizableSpace Y

theorem PiBase.WellDefined.isCompletelyMetrizableSpace : WellDefined TopologicalSpace.IsCompletelyMetrizableSpace