theorem PiBase.WellDefined.preconnectedSpace : WellDefined PreconnectedSpace

theorem PiBase.Homeomorph.preconnectedSpace {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] [PreconnectedSpace X] (f : X ≃ₜ Y) : PreconnectedSpace Y