isGenericPoint_ofComponent — Mathlib

English

Every irreducible component has a generic point: IsGenericPoint((ofComponent x).1, x) for x in irreducibleComponents α.

Русский

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

LaTeX

$$$IsGenericPoint((ofComponent x).1, x)$ for all $x$ in $(irreducibleComponents(\\alpha)).$$$

Lean4

theorem isGenericPoint_ofComponent [QuasiSober α] (x : irreducibleComponents α) : IsGenericPoint (ofComponent x).1 x :=
  x.2.1.isGenericPoint_genericPoint (isClosed_of_mem_irreducibleComponents x.1 x.2)

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