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

139. Has an isolated point

• ex_isolated : ∃ (x : X), IsOpen {x}