English
There exists an order isomorphism between the poset of irreducible closed subsets of a topological space α and the collection of pairs (X, h) where X ⊆ α is irreducible and closed. Concretely, each irreducible closed set corresponds to its underlying set, and conversely each irreducible closed subset is mapped to the pair consisting of that set and its properties.
Русский
Существует упорядоченный изоморфизм между частично упорядоченным множеством неразложимых замкнутых подмножеств пространства топологического типа α и множеством пар (X, h), где X ⊆ α является неразложимым и замкнутым. Каждое неразложимое замкнутое множество сопоставляется своему множества-основе, и наоборот каждое такое подмножество сопоставляется паре, включающей само множество и соответствующие свойства.
LaTeX
$$$\mathrm{IrreducibleCloseds}(\alpha) \cong_o \{ x \subseteq \alpha \mid \mathrm{IsIrreducible}(x) \wedge \mathrm{IsClosed}(x) \}$$$
Lean4
/-- The equivalence `IrreducibleCloseds α ≃ { x : Set α // IsIrreducible x ∧ IsClosed x }` is an
order isomorphism. -/
def orderIsoSubtype : IrreducibleCloseds α ≃o { x : Set α // IsIrreducible x ∧ IsClosed x } :=
equivSubtype.toOrderIso (fun _ _ h ↦ h) (fun _ _ h ↦ h)
