ofComponent_component — Mathlib

English

The composite of the forward and backward maps on irreducible components is the identity on genericPoints: ofComponent (component x) = x.

Русский

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

LaTeX

$$$\\text{ofComponent}(\\text{component}(x)) = x$ for any x in genericPoints α.$$

Lean4

@[simp]
theorem ofComponent_component [T0Space α] [QuasiSober α] (x : genericPoints α) : ofComponent (component x) = x :=
  component_injective (component_ofComponent _)

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