English
Let α be a topological space. If α is a T0 space and the set of irreducible components of α is finite, then the set of generic points of α is finite.
Русский
Пусть α — топологическое пространство. Если α является T0-пространством и множество неразложимых компонент α конечно, то множество генерических точек α конечно.
LaTeX
$$$[T_0\text{-space }\alpha]\;\Rightarrow\;((\operatorname{irreducibleComponents}(\alpha)).\Finite)\Rightarrow ((\operatorname{genericPoints}(\alpha)).\Finite)$$$
Lean4
theorem finite [T0Space α] (h : (irreducibleComponents α).Finite) : (genericPoints α).Finite :=
@Finite.of_injective _ _ h _ component_injective
