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

• locally_contractible (x : X) : (nhds x).HasBasis (fun (s : Set X) => IsOpen s ∧ x ∈ s ∧ ContractibleSpace ↑s) id