irreducibleComponents_eq_singleton

English

If X is irreducible, then the irreducible components of X are just {univ}.

Русский

Если X неразложимо, то единственная компонента неразложимости — это X.

LaTeX

$$[\mathrm{IrreducibleSpace}(X)] \Rightarrow \mathrm{irreducibleComponents}(X) = \{\mathrm{univ}\}$$

Lean4

theorem irreducibleComponents_eq_singleton [IrreducibleSpace X] : irreducibleComponents X = { univ } :=
  Set.ext fun _ ↦
    IsGreatest.maximal_iff (s := IsIrreducible (X := X))
      ⟨IrreducibleSpace.isIrreducible_univ X, fun _ _ ↦ Set.subset_univ _⟩

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