ofComponent — Mathlib

English

Given an irreducible component, one can take its generic point to obtain an element of genericPoints α.

Русский

Заданному неразложимому компоненту соответствует его генерирующая точка в genericPoints α.

LaTeX

$$$(\\text{ofComponent} : (irreducibleComponents(\\alpha)).Elem \\to (genericPoints(\\alpha)).Elem)$ is well-defined.$$

Lean4

/-- The generic point of an irreducible component. -/
noncomputable def ofComponent [QuasiSober α] (x : irreducibleComponents α) : genericPoints α :=
  ⟨x.2.1.genericPoint,
    show _ ∈ irreducibleComponents α from
      (x.2.1.isGenericPoint_genericPoint (isClosed_of_mem_irreducibleComponents x.1 x.2)).symm ▸ x.2⟩

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