component_surjective — Mathlib

English

The map component: genericPoints α → irreducibleComponents α is surjective; every irreducible component is the image of some generic point.

Русский

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

LaTeX

$$$\\text{component}:\\text{genericPoints}(\\alpha) \\to (\\text{irreducibleComponents}(\\alpha))$ is surjective.$$

Lean4

theorem component_surjective [QuasiSober α] : Function.Surjective (component (α := α)) :=
  Function.HasRightInverse.surjective ⟨ofComponent, component_ofComponent⟩

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