component_ofComponent — Mathlib

English

The generic point of the irreducible component, mapped back, returns to the original irreducible component: (genericPoints.component (genericPoints.ofComponent x)) = x.

Русский

Генерирующая точка неразложимого компонента, возвращенная через компоненту обратно, возвращает исходный компонент.

LaTeX

$$$\\text{component}(\\text{ofComponent}(x)) = x$ for all x in irreducibleComponents α.$$

Lean4

@[simp]
theorem component_ofComponent [QuasiSober α] (x : irreducibleComponents α) : component (ofComponent x) = x :=
  Subtype.ext (isGenericPoint_ofComponent x)

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