finite_irreducibleComponents — Mathlib

English

In a Noetherian space, the collection of irreducible components is finite.

Русский

В Noetherian-пространстве множество неприводимых компонент конечно.

LaTeX

$$$\operatorname{Finite}(\operatorname{irreducibleComponents}(X)).$$$

Lean4

@[stacks 0052 "(2)"]
theorem finite_irreducibleComponents [NoetherianSpace α] : (irreducibleComponents α).Finite :=
  by
  obtain ⟨S : Set (Set α), hSf, hSc, hSi, hSU⟩ :=
    NoetherianSpace.exists_finite_set_isClosed_irreducible isClosed_univ (α := α)
  refine hSf.subset fun s hs => ?_
  lift S to Finset (Set α) using hSf
  rcases isIrreducible_iff_sUnion_isClosed.1 hs.1 S hSc (hSU ▸ Set.subset_univ _) with ⟨t, htS, ht⟩
  rwa [ht.antisymm (hs.2 (hSi _ htS) ht)]

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