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

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