genericPoints — Mathlib

English

The set of generic points consists of those x with closure{x} an irreducible component.

Русский

Множество генерирующих точек состоит из тех x, для которых closure{ x } — неразложимый компонент.

LaTeX

$$$\\text{genericPoints}(\\alpha) = \\{ x \\in \\alpha \\mid \\overline{\\{x\\}} \\in \\operatorname{irreducibleComponents}(\\alpha) \\}$$$

Lean4

/-- The set of generic points of irreducible components. -/
def genericPoints : Set α :=
  {x | closure { x } ∈ irreducibleComponents α}

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