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

• ex_point : ∃ (p : X), ∀ (x : X), x ≠ p ↔ IsOpen {x}