English
In a Noetherian space, every closed set can be written as a finite union of irreducible closed sets; equivalently, there exist finitely many closed irreducible subsets whose union is the given set.
Русский
В Noetherian-пространстве любое замкнутое множество может быть представлено как конечное объединение неприводимых замкнутых подмножеств.
LaTeX
$$$\forall s \subseteq X, \text{IsClosed}(s) \Rightarrow \exists \{T_1, \dots, T_m\}, \ T_i \text{ closed irreducible}, \ s = \bigcup_{i=1}^m T_i.$$$
Lean4
/-- In a Noetherian space, every closed set is a finite union of irreducible closed sets. -/
theorem exists_finite_set_isClosed_irreducible [NoetherianSpace α] {s : Set α} (hs : IsClosed s) :
∃ S : Set (Set α), S.Finite ∧ (∀ t ∈ S, IsClosed t) ∧ (∀ t ∈ S, IsIrreducible t) ∧ s = ⋃₀ S :=
by
lift s to Closeds α using hs
rcases NoetherianSpace.exists_finite_set_closeds_irreducible s with ⟨S, hSf, hS, rfl⟩
refine ⟨(↑) '' S, hSf.image _, Set.forall_mem_image.2 fun S _ ↦ S.2, Set.forall_mem_image.2 hS, ?_⟩
lift S to Finset (Closeds α) using hSf
simp [← Finset.sup_id_eq_sSup, Closeds.coe_finset_sup]
