theorem PiBase.isPreirreducible_iff_subset_closure_inter_open {X : Type u_1} [TopologicalSpace X] (S : Set X) : IsPreirreducible S ↔ ∀ (U : Set X), IsOpen U → (S ∩ U).Nonempty → S ⊆ closure (S ∩ U)

theorem PiBase.preirreducibleSpace_iff_open_dense (X : Type u_3) [TopologicalSpace X] : PreirreducibleSpace X ↔ ∀ ⦃U : Set X⦄, IsOpen U → U.Nonempty → Dense U

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

theorem PiBase.WellDefined.preirreducibleSpace : WellDefined PreirreducibleSpace