genericPoint_spec — Mathlib

English

In a sober irreducible space α, the genericPoint of α is a generic point for the entire space univ.

Русский

В безразделяемом пространстве α существующая генерирующая точка является генерирующей точкой для всего пространства.

LaTeX

$$$IsGenericPoint(genericPoint(\\alpha), univ).$$$

Lean4

theorem genericPoint_spec [QuasiSober α] [IrreducibleSpace α] : IsGenericPoint (genericPoint α) univ := by
  simpa using (IrreducibleSpace.isIrreducible_univ α).isGenericPoint_genericPoint_closure

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