class PiBase.WeaklyLocallyContractibleSpace (X : Type u) [TopologicalSpace X] : Prop

• weakly_locally_contractible (x : X) : ∃ s ∈ nhds x, ContractibleSpace ↑s