genericPoints_eq_singleton — Mathlib

English

If α is quasi-sober, irreducible, and T0, then the set of generic points of α is a singleton, namely {genericPoint(α)}.

Русский

Если α квазисобово и неприведимо, и T0, тогда множество генерических точек α является одиноким множеством {genericPoint(α)}.

LaTeX

$$$[QuasiSober(\alpha)]\ [IrreducibleSpace(\alpha)]\ [T0Space(\alpha)]:\; \mathrm{genericPoints}(\alpha) = \{ \mathrm{genericPoint}(\alpha) \}$$$

Lean4

theorem genericPoints_eq_singleton [QuasiSober α] [IrreducibleSpace α] [T0Space α] :
    genericPoints α = {genericPoint α} := by
  ext x
  rw [genericPoints, irreducibleComponents_eq_singleton]
  exact ⟨((genericPoint_spec α).eq · |>.symm), (· ▸ genericPoint_spec α)⟩

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