English
Let α be a topological space that is T0 and quasi-sober. Then there is a natural bijection between the set of generic points of α and the set of irreducible components of α.
Русский
Пусть α — топологическое пространство, являющееся T0 и квазисоберным. Тогда существует естественная биекция между множеством генерических точек α и множеством неразложимых компонент α.
LaTeX
$$$[T_0\text{-space }\alpha]\;[\text{QuasiSober }\alpha]\;:\; (genericPoints(\alpha)) \cong (irreducibleComponents(\alpha))$$$
Lean4
/-- In a sober space, the generic points corresponds bijectively to irreducible components -/
@[simps]
noncomputable def equiv [T0Space α] [QuasiSober α] : genericPoints α ≃ irreducibleComponents α :=
⟨component, ofComponent, ofComponent_component, component_ofComponent⟩
