class PiBase.WeaklyLocallySimplyConnectedSpace (X : Type u_1) [TopologicalSpace X] : Prop

• simply_connected_nbhd (x : X) : ∃ U ∈ nhds x, SimplyConnectedSpace ↑U