exists_finset_irreducible — Mathlib

English

In a Noetherian space, every closed set s can be expressed as a finite union of irreducible closed sets.

Русский

В Noetherian-пространстве каждое замкнутое множество может быть представлено как конечное объединение неприводимых замкнутых множеств.

LaTeX

$$$\forall s \in \operatorname{Closeds}(X), \exists S \subseteq \operatorname{Closeds}(X), S \text{ finite}, \forall t \in S, \operatorname{IsIrreducible}(t), \ s = \bigcup S.$$$

Lean4

/-- In a Noetherian space, every closed set is a finite union of irreducible closed sets. -/
theorem exists_finset_irreducible [NoetherianSpace α] (s : Closeds α) :
    ∃ S : Finset (Closeds α), (∀ k : S, IsIrreducible (k : Set α)) ∧ s = S.sup id := by
  simpa [Set.exists_finite_iff_finset, Finset.sup_id_eq_sSup] using
    NoetherianSpace.exists_finite_set_closeds_irreducible s

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