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

theorem PiBase.WellDefined.r0Space : WellDefined R0Space