theorem PiBase.Homeomorph.hereditarilyConnected {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [HereditarilyConnected X] (φ : X ≃ₜ Y) : HereditarilyConnected Y

theorem PiBase.WellDefined.hereditarilyConnected : WellDefined HereditarilyConnected