theorem PiBase.Formal.hasCoarserSeparableMetrizableTopology_of_homeomorph {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (φ : X ≃ₜ Y) (h : HasCoarserSeparableMetrizableTopology X) : HasCoarserSeparableMetrizableTopology Y

theorem PiBase.Formal.P166.well_defined {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (φ : X ≃ₜ Y) (h : HasCoarserSeparableMetrizableTopology X) : HasCoarserSeparableMetrizableTopology Y

theorem PiBase.WellDefined.hasCoarserSeparableMetrizableTopology : WellDefined HasCoarserSeparableMetrizableTopology