theorem IsPreirreducible.of_subtype {X : Type u_1} [TopologicalSpace X] (s : Set X) [PreirreducibleSpace ↑s] : IsPreirreducible s

theorem IsIrreducible.of_subtype {X : Type u_1} [TopologicalSpace X] (s : Set X) [IrreducibleSpace ↑s] : IsIrreducible s

theorem IsPreirreducible.of_isOpen {X : Type u_1} [TopologicalSpace X] [PreirreducibleSpace X] (U : Set X) (h : IsOpen U) : IsPreirreducible U

@[instance 100]

instance PreirreducibleSpace.of_isEmpty (X : Type u_1) [TopologicalSpace X] [IsEmpty X] : PreirreducibleSpace X

theorem isIrreducible_of_mem_irreducibleComponents {X : Type u_1} [TopologicalSpace X] {s : Set X} (hs : s ∈ irreducibleComponents X) : IsIrreducible s

theorem irreducibleComponents_eq_singleton_iff {X : Type u_1} [TopologicalSpace X] : irreducibleComponents X = {Set.univ} ↔ IrreducibleSpace X

theorem irreducibleSpace_iff_nonempty_and_subsingleton {X : Type u_1} [TopologicalSpace X] : IrreducibleSpace X ↔ Nonempty X ∧ (irreducibleComponents X).Subsingleton

theorem preirreducibleSpace_iff_subsingleton_irreducibleComponents {X : Type u_1} [TopologicalSpace X] : PreirreducibleSpace X ↔ (irreducibleComponents X).Subsingleton

theorem Function.Surjective.preirreducibleSpace {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) (hfc : Continuous f) (hf : Surjective f) [PreirreducibleSpace X] : PreirreducibleSpace Y

theorem Function.Surjective.irreducibleSpace {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) (hfc : Continuous f) (hf : Surjective f) [IrreducibleSpace X] : IrreducibleSpace Y

theorem PreirreducibleSpace.of_forall_nonempty_inter {X : Type u_1} [TopologicalSpace X] (H : ∀ ⦃U V : Set X⦄, IsOpen U → IsOpen V → U.Nonempty → V.Nonempty → (U ∩ V).Nonempty) : PreirreducibleSpace X

theorem IsOpenMap.denseRange_of_isPreirreducibleSpace {U : Type u_1} {X : Type u_2} [TopologicalSpace U] [Nonempty U] [TopologicalSpace X] (f : U → X) (hf : IsOpenMap f) [PreirreducibleSpace X] : DenseRange f

theorem Topology.IsOpenEmbedding.preirreducibleSpace {U : Type u_1} {X : Type u_2} [TopologicalSpace U] [TopologicalSpace X] {f : U → X} (hf : IsOpenEmbedding f) [PreirreducibleSpace X] : PreirreducibleSpace U

theorem Topology.IsOpenEmbedding.irreducibleSpace {U : Type u_1} {X : Type u_2} [TopologicalSpace U] [TopologicalSpace X] {f : U → X} (hf : IsOpenEmbedding f) [IrreducibleSpace X] [Nonempty U] : IrreducibleSpace U

theorem IrreducibleSpace.of_openCover {X : Type u_1} {ι : Type u_2} [TopologicalSpace X] [hι : Nonempty ι] {U : ι → TopologicalSpace.Opens X} (hU : TopologicalSpace.IsOpenCover U) (hn : ∀ (i j : ι), ((U i).carrier ∩ (U j).carrier).Nonempty) (h : ∀ (i : ι), IrreducibleSpace ↥(U i)) : IrreducibleSpace X

Irreducibility can be checked on an open cover with pairwise non-empty intersections.