English
Let α be a quasi-sober topological space. If S ⊆ α is irreducible, then there exists a point x in the closure of S such that the closure of {x} equals the closure of S. In other words, the closure of S has a generic point.
Русский
Пусть α — топологическое пространство с квази-собростью. Если S ⊆ α неразложимо, то существует точка x в замыкании S такая, что замыкание {x} равно замыканию S; то есть замыкание S имеет генерирующую точку.
LaTeX
$$$\\exists x \\in \\overline{S} \\;\\text{such that}\\; \\overline{\\{x\\}} = \\overline{S}. $$$
Lean4
/-- A generic point of the closure of an irreducible space. -/
noncomputable def genericPoint [QuasiSober α] {S : Set α} (hS : IsIrreducible S) : α :=
(QuasiSober.sober hS.closure isClosed_closure).choose
