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

• ex_point_unique_nbhd : ∃ (p : X), nhds p = ⊤