component — Mathlib

English

For a generic point x ∈ genericPoints α, the component of x is the irreducible component given by the closure of {x}.

Русский

Для генерик точки x в genericPoints α компонентом x является неразложимый компонент, задаваемый замыканием {x}.

LaTeX

$$$\\text{component}(x) = \\langle \\overline{\\{x\\}}, x.2\\rangle$ for $x \\in genericPoints(\\alpha)$.$$

Lean4

/-- The irreducible component of a generic point -/
def component (x : genericPoints α) : irreducibleComponents α :=
  ⟨closure { x.1 }, x.2⟩

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