theorem PiBase.semilocallySimplyConnectedSpace_of_homeomorph {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ₜ Y) (h : SemilocallySimplyConnectedSpace X) : SemilocallySimplyConnectedSpace Y

Semilocal simple connectedness is transported along a homeomorphism.

Given U ∈ 𝓝 (e.symm y) witnessing the property at e.symm y, the neighbourhood e.symm ⁻¹' U ∈ 𝓝 y works at y: its inclusion into Y factors as e ∘ (U ↪ X) ∘ (e.symm ⁻¹' U ≃ₜ U), so functoriality of FundamentalGroup.map kills it.

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

theorem PiBase.WellDefined.semilocallySimplyConnectedSpace : WellDefined SemilocallySimplyConnectedSpace