English
Let α be a quasi-sober topological space. Then the closure of the set of generic points of α is the whole space; equivalently, generic points are dense in α.
Русский
Пусть α — квазисобовое топологическое пространство. Тогда замыкание множества генерических точек α равно всему пространству; эквивалентно тому, что генерические точки плотны в α.
LaTeX
$$$[QuasiSober(\alpha)]\;:\; \mathrm{cl}(\mathrm{genericPoints}(\alpha)) = \mathrm{univ}$$$
Lean4
theorem closure [QuasiSober α] : closure (genericPoints α) = Set.univ :=
by
refine Set.eq_univ_iff_forall.mpr fun x ↦ Set.subset_def.mp ?_ x mem_irreducibleComponent
refine
(isGenericPoint_ofComponent ⟨_, irreducibleComponent_mem_irreducibleComponents x⟩).symm.trans_subset
(closure_mono ?_)
exact Set.singleton_subset_iff.mpr (ofComponent _).2
