no goals
α : Type u_1
β : Type ?u.17376
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : NoetherianSpace α
s : Closeds α
⊢ ∃ S, (∀ (k : { x // x ∈ S }), IsIrreducible ↑↑k) ∧ s = Finset.sup S id
simpa [Set.exists_finite_iff_finset, Finset.sup_id_eq_sSup]
  using NoetherianSpace.exists_finite_set_closeds_irreducible s