def IsIrreducibleComponentOf {X : Type u_1} [TopologicalSpace X] (s : Set X) : Prop

Irreducible component (Def 8, Lec 3): a subset s ⊆ X is an irreducible component if it is a maximal irreducible closed subset of X.

theorem isIrreducibleComponentOf_iff_maximal_closed_irreducible {X : Type u_1} [TopologicalSpace X] (s : Set X) : IsIrreducibleComponentOf s ↔ Maximal (fun (t : Set X) => IsClosed t ∧ IsIrreducible t) s

Characterization: s is an irreducible component iff s is maximal among closed irreducible subsets.

theorem IsIrreducibleComponentOf.isIrreducible {X : Type u_1} [TopologicalSpace X] {s : Set X} (hs : IsIrreducibleComponentOf s) : IsIrreducible s

An irreducible component is irreducible.

theorem IsIrreducibleComponentOf.isClosed {X : Type u_1} [TopologicalSpace X] {s : Set X} (hs : IsIrreducibleComponentOf s) : IsClosed s

An irreducible component is closed.

theorem exists_irreducibleComponent_superset {X : Type u_1} [TopologicalSpace X] {s : Set X} (hs : IsIrreducible s) : ∃ (t : Set X), IsIrreducibleComponentOf t ∧ s ⊆ t

Every irreducible subset is contained in some irreducible component.

theorem exists_irreducibleComponent_of_mem {X : Type u_1} [TopologicalSpace X] (x : X) : ∃ (s : Set X), IsIrreducibleComponentOf s ∧ x ∈ s

Every point of X is contained in some irreducible component.