theorem PiBase.soberSpace_iff_ex_unique_generic {X : Type u_1} [TopologicalSpace X] : SoberSpace X ↔ ∀ (S : Set X), IsIrreducible S → IsClosed S → ∃! x : X, IsGenericPoint x S

theorem PiBase.Homeomorph.soberSpace {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [h : SoberSpace X] (f : X ≃ₜ Y) : SoberSpace Y

theorem PiBase.WellDefined.soberSpace : WellDefined SoberSpace