English
The irreducible components are exactly the maximal closed irreducible subsets.
Русский
Неразложимые компоненты являются ровно максимальными замкнутыми неразложимыми подмножествами.
LaTeX
$$$\\operatorname{irreducibleComponents}(X) = \\{ s \\mid \\operatorname{Maximal}(\\lambda x: IsClosed(x) \\wedge \\operatorname{IsIrreducible}(x))\\, s \\}$$$
Lean4
theorem irreducibleComponents_eq_maximals_closed (X : Type*) [TopologicalSpace X] :
irreducibleComponents X = {s | Maximal (fun x ↦ IsClosed x ∧ IsIrreducible x) s} :=
by
ext s
constructor
· intro H
exact ⟨⟨isClosed_of_mem_irreducibleComponents _ H, H.1⟩, fun x h e => H.2 h.2 e⟩
· intro H
refine ⟨H.1.2, fun x h e => ?_⟩
have : closure x ≤ s := H.2 ⟨isClosed_closure, h.closure⟩ (e.trans subset_closure)
exact le_trans subset_closure this
