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

theorem PiBase.WellDefined.isEmpty : WellDefined fun (X : Type u_3) [TopologicalSpace X] => IsEmpty X