English
There is an order isomorphism between the poset of irreducible closeds in α and the subset of Set α consisting of closed irreducible subsets. It maps each irreducible closed set to its underlying set and back via the closure/irreducibility data.
Русский
Существует упорядоченный изоморфизм между множеством ирредуцируемых замкнутых множеств в пространстве α и подмножеством множества α, состоящим из замкнутых неразложимых подмножеств. Он отправляет каждое неразложимое замкнутое множество на его основание и обратно через данные замкнутости и ирредуцируемости.
LaTeX
$$$\mathrm{IrreducibleCloseds}(\alpha) \cong_o \{ x \subseteq \alpha \mid \mathrm{IsClosed}(x) \wedge \mathrm{IsIrreducible}(x) \}$$$
Lean4
/-- The equivalence `IrreducibleCloseds α ≃ { x : Set α // IsClosed x ∧ IsIrreducible x }` is an
order isomorphism. -/
def orderIsoSubtype' : IrreducibleCloseds α ≃o { x : Set α // IsClosed x ∧ IsIrreducible x } :=
equivSubtype'.toOrderIso (fun _ _ h ↦ h) (fun _ _ h ↦ h)
