English
In a Noetherian topological space, every closed set is a finite union of irreducible closed sets.
Русский
В Noetherian-пространстве каждоe замкнутое множество является конечным объединением неприводимых замкнутых множеств.
LaTeX
$$$\forall X$-Noetherian, \; \forall s \text{ closed in } X, \; \exists \{F_1, \dots, F_n\}, \ F_i \text{ irreducible closed}, \ s = \bigcup_{i=1}^n F_i.$$$
Lean4
/-- In a Noetherian space, every closed set is a finite union of irreducible closed sets. -/
theorem exists_finite_set_closeds_irreducible [NoetherianSpace α] (s : Closeds α) :
∃ S : Set (Closeds α), S.Finite ∧ (∀ t ∈ S, IsIrreducible (t : Set α)) ∧ s = sSup S :=
by
apply wellFounded_lt.induction s; clear s
intro s H
rcases eq_or_ne s ⊥ with rfl | h₀
· use ∅; simp
· by_cases h₁ : IsPreirreducible (s : Set α)
· replace h₁ : IsIrreducible (s : Set α) := ⟨Closeds.coe_nonempty.2 h₀, h₁⟩
use { s }; simp [h₁]
· simp only [isPreirreducible_iff_isClosed_union_isClosed, not_forall, not_or] at h₁
obtain ⟨z₁, z₂, hz₁, hz₂, h, hz₁', hz₂'⟩ := h₁
lift z₁ to Closeds α using hz₁
lift z₂ to Closeds α using hz₂
rcases H (s ⊓ z₁) (inf_lt_left.2 hz₁') with ⟨S₁, hSf₁, hS₁, h₁⟩
rcases H (s ⊓ z₂) (inf_lt_left.2 hz₂') with ⟨S₂, hSf₂, hS₂, h₂⟩
refine ⟨S₁ ∪ S₂, hSf₁.union hSf₂, Set.union_subset_iff.2 ⟨hS₁, hS₂⟩, ?_⟩
rwa [sSup_union, ← h₁, ← h₂, ← inf_sup_left, left_eq_inf]
