component_injective — Mathlib

English

The map that assigns to a generic point its irreducible component is injective when α is T0.

Русский

Отображение, сопоставляющее генерирующей точке её неразложимый компоненту, инъективно при условии T0 пространства.

LaTeX

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

Lean4

theorem component_injective [T0Space α] : Function.Injective (component (α := α)) := fun x y e ↦
  Subtype.ext ((isGenericPoint x).eq (e ▸ isGenericPoint y))

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