isGenericPoint_genericPoint_closure

English

In a quasi-sober space, for every irreducible subset S, there is a generic point for its closure. Equivalently, closure of some point equals closure of S.

Русский

В полуздравляемом пространстве существует генерирующая точка для замыкания любой неразложимой подсистемы S.

LaTeX

$$$\\text{If } S \\subseteq \\alpha \\text{ is irreducible, then } \\exists x: \\overline{\\{x\\}} = \\overline{S}.$$$

Lean4

theorem isGenericPoint_genericPoint_closure [QuasiSober α] {S : Set α} (hS : IsIrreducible S) :
    IsGenericPoint hS.genericPoint (closure S) :=
  (QuasiSober.sober hS.closure isClosed_closure).choose_spec

Похожие утверждения