Irreducible space (Def 7, Lec 3): X is irreducible iff the whole space ⊤ is
irreducible as a subset.
theorem
IrreducibleSpace.nonempty_inter_of_open
{X : Type u_1}
[TopologicalSpace X]
[IrreducibleSpace X]
{U V : Set X}
(hU : IsOpen U)
(hV : IsOpen V)
(hU' : U.Nonempty)
(hV' : V.Nonempty)
:
In an irreducible space, any two nonempty open sets meet (Def 7, Lec 3).
theorem
IrreducibleSpace.eq_univ_of_isClosed_union
{X : Type u_1}
[TopologicalSpace X]
[IrreducibleSpace X]
{Z₁ Z₂ : Set X}
(hZ₁ : IsClosed Z₁)
(hZ₂ : IsClosed Z₂)
(h : Z₁ ∪ Z₂ = Set.univ)
:
Dual form: if X is irreducible and X = Z₁ ∪ Z₂ with Zᵢ closed, then one of
the Zᵢ is the whole space.
theorem
IrreducibleSpace.dense_of_isOpen
{X : Type u_1}
[TopologicalSpace X]
[IrreducibleSpace X]
{U : Set X}
(hU : IsOpen U)
(hne : U.Nonempty)
:
Dense U
In an irreducible space, every nonempty open set is dense.