genericPoint — Mathlib

English

A sober irreducible space has a canonical generic point for the whole space: there exists x ∈ α with closure{x} = α.

Русский

В безраздельно-топологическом пространстве (соборном и неразложимом) существует генерирующая точка всего пространства: найдется x такой, что closures{x} = α.

LaTeX

$$$\\exists x \\in \\alpha:\\; \\overline{\\{x\\}} = \\alpha.$$$

Lean4

/-- A generic point of a sober irreducible space. -/
noncomputable def genericPoint [QuasiSober α] [IrreducibleSpace α] : α :=
  (IrreducibleSpace.isIrreducible_univ α).genericPoint

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