Irreducibility from a cover by pairwise-meeting irreducible opens

A space covered by preirreducible opens that pairwise intersect is preirreducible. This is the form the projective spectrum needs: Proj 𝒜 of a graded domain is covered by the basic opens D₊(f), each the spectrum of a domain and so irreducible, and any two of them meet because the product of two nonzero homogeneous elements is nonzero.

Mathlib has the irreducibility of Spec of a domain and the local-to-global machinery for schemes, but not this purely topological step.

theorem TopologicalSpace.isPreirreducible_univ_of_cover {X : Type u_1} [TopologicalSpace X] {ind : Type u_2} (U : ind → Set X) (hopen : ∀ (i : ind), IsOpen (U i)) (hcover : ∀ (x : X), ∃ (i : ind), x ∈ U i) (hirred : ∀ (i : ind), IsPreirreducible (U i)) (hmeet : ∀ (i j : ind), (U i ∩ U j).Nonempty) : IsPreirreducible Set.univ

A cover by preirreducible open sets that pairwise intersect makes the whole space preirreducible.

theorem TopologicalSpace.irreducibleSpace_of_cover {X : Type u_1} [TopologicalSpace X] {ind : Type u_2} [Nonempty X] (U : ind → Set X) (hopen : ∀ (i : ind), IsOpen (U i)) (hcover : ∀ (x : X), ∃ (i : ind), x ∈ U i) (hirred : ∀ (i : ind), IsPreirreducible (U i)) (hmeet : ∀ (i j : ind), (U i ∩ U j).Nonempty) : IrreducibleSpace X

The bundled form, adding the nonemptiness IrreducibleSpace demands.

Nonemptiness does not follow from the hypotheses: an empty cover over an empty index type satisfies all of them vacuously.