class PiBase.HasDispersionPoint (X : Type u_1) [TopologicalSpace X] extends ConnectedSpace X : Prop

• isPreconnected_univ : IsPreconnected Set.univ
• toNonempty : Nonempty X
• ex_dispersion_point : ∃ (p : X), IsTotallyDisconnected {p}ᶜ