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

• inj_path_connected_basis (x : X) : (nhds x).HasBasis (fun (s : Set X) => x ∈ s ∧ IsOpen s ∧ IsInjPathConnected s) id