genericPoint_closure — Mathlib

English

For sober irreducible α, the generic point of α has closure equal to the whole space, i.e., closure({genericPoint α}) = univ.

Русский

Для собренного неразложимого пространства α замыкание {генерирующая точка α} равно всего пространства.

LaTeX

$$$\\overline{\\{genericPoint(\\alpha)\\}} = univ$$$

Lean4

@[simp]
theorem genericPoint_closure [QuasiSober α] [IrreducibleSpace α] : closure ({genericPoint α} : Set α) = univ :=
  genericPoint_spec α

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