class PiBase.SoberSpace (X : Type u_1) [TopologicalSpace X] extends QuasiSober X, T0Space X : Prop

• sober {S : Set X} : IsIrreducible S → IsClosed S → ∃ (x : X), IsGenericPoint x S
• t0 ⦃x y : X⦄ : Inseparable x y → x = y