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

• locally_relatively_compact (x : X) : (nhds x).HasBasis (fun (s : Set X) => s ∈ nhds x ∧ IsCompact (closure s)) id