∀ {X : Type u_1} {ι : Type u_2} [inst : TopologicalSpace X] {U : ι → TopologicalSpace.Opens X},
  Pairwise (Function.onFun (fun x1 x2 => ¬Disjoint x1 x2) U) →
    TopologicalSpace.IsOpenCover U → (∀ (i : ι), PreirreducibleSpace ↥(U i)) → PreirreducibleSpace X