theorem PiBase.isInjPathConnectedSpace_of_injective_image {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (fc : Continuous f) {s : Set X} (fs : Set.InjOn f s) (hs : IsInjPathConnected s) : IsInjPathConnected (f '' s)

theorem PiBase.injPathConnectedSpace_of_bijective_continuous {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [h : InjPathConnectedSpace X] {f : X → Y} (fc : Continuous f) (fb : Function.Bijective f) : InjPathConnectedSpace Y

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

theorem PiBase.WellDefined.injPathConnectedSpace : WellDefined InjPathConnectedSpace

theorem PiBase.isInjPathConnected_iff_injPathConnectedSpace {X : Type u_1} [TopologicalSpace X] (s : Set X) : IsInjPathConnected s ↔ InjPathConnectedSpace ↑s