diff --git a/Mathlib.lean b/Mathlib.lean
index c985dd059537e6..2448d9a560ce20 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -3374,6 +3374,7 @@ import Mathlib.Data.Set.Constructions
 import Mathlib.Data.Set.Countable
 import Mathlib.Data.Set.Defs
 import Mathlib.Data.Set.Disjoint
+import Mathlib.Data.Set.Dissipate
 import Mathlib.Data.Set.Enumerate
 import Mathlib.Data.Set.Equitable
 import Mathlib.Data.Set.Finite.Basic
@@ -6104,6 +6105,7 @@ import Mathlib.Topology.Compactification.OnePoint.Sphere
 import Mathlib.Topology.Compactification.OnePointEquiv
 import Mathlib.Topology.Compactness.Bases
 import Mathlib.Topology.Compactness.Compact
+import Mathlib.Topology.Compactness.CompactSystem
 import Mathlib.Topology.Compactness.CompactlyCoherentSpace
 import Mathlib.Topology.Compactness.CompactlyGeneratedSpace
 import Mathlib.Topology.Compactness.DeltaGeneratedSpace
diff --git a/Mathlib/Data/Set/Accumulate.lean b/Mathlib/Data/Set/Accumulate.lean
index 64d874f0e99e64..62c13904f1e9e1 100644
--- a/Mathlib/Data/Set/Accumulate.lean
+++ b/Mathlib/Data/Set/Accumulate.lean
@@ -8,7 +8,11 @@ import Mathlib.Data.Set.Lattice
 /-!
 # Accumulate
 
-The function `Accumulate` takes a set `s` and returns `⋃ y ≤ x, s y`.
+The function `Accumulate` takes `s : α → Set β` with `LE α` and returns `⋃ y ≤ x, s y`.
+
+In large parts, this file is parallel to `Mathlib.Data.Set.Dissipate`, where
+`Dissipate s := ⋂ y ≤ x, s y` is defined.
+
 -/
 
 
@@ -16,7 +20,7 @@ variable {α β : Type*} {s : α → Set β}
 
 namespace Set
 
-/-- `Accumulate s` is the union of `s y` for `y ≤ x`. -/
+/-- `Accumulate s x` is the union of `s y` for `y ≤ x`. -/
 def Accumulate [LE α] (s : α → Set β) (x : α) : Set β :=
   ⋃ y ≤ x, s y
 
diff --git a/Mathlib/Data/Set/Dissipate.lean b/Mathlib/Data/Set/Dissipate.lean
new file mode 100644
index 00000000000000..43c4ecb7848536
--- /dev/null
+++ b/Mathlib/Data/Set/Dissipate.lean
@@ -0,0 +1,157 @@
+/-
+Copyright (c) 2025 Peter Pfaffelhuber. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Peter Pfaffelhuber
+-/
+import Mathlib.Data.Set.Lattice
+import Mathlib.Order.Directed
+import Mathlib.MeasureTheory.PiSystem
+
+/-!
+# Dissipate
+
+The function `Dissipate` takes `s : α → Set β` with `LE α` and returns `⋂ y ≤ x, s y`.
+
+In large parts, this file is parallel to `Mathlib.Data.Set.Accumulate`, where
+`Accumulate s := ⋃ y ≤ x, s y` is defined.
+
+-/
+
+open Nat
+
+variable {α β : Type*} {s : α → Set β}
+
+namespace Set
+
+/-- `Dissipate s x` is the intersection of `s y` for `y ≤ x`. -/
+def Dissipate [LE α] (s : α → Set β) (x : α) : Set β :=
+  ⋂ y ≤ x, s y
+
+theorem dissipate_def [LE α] {x : α} : Dissipate s x = ⋂ y ≤ x, s y := rfl
+
+theorem dissipate_eq {s : ℕ → Set β} {n : ℕ} : Dissipate s n = ⋂ k < n + 1, s k := by
+  simp_rw [Nat.lt_add_one_iff]
+  rfl
+
+theorem mem_dissipate [LE α] {x : α} {z : β} : z ∈ Dissipate s x ↔ ∀ y ≤ x, z ∈ s y := by
+  simp only [dissipate_def, mem_iInter]
+
+theorem dissipate_subset [Preorder α] {x y : α} (hy : y ≤ x) : Dissipate s x ⊆ s y :=
+  biInter_subset_of_mem hy
+
+theorem dissipate_subset_iInter [Preorder α] (x : α) : ⋂ i, s i ⊆ Dissipate s x := by
+  simp only [Dissipate, subset_iInter_iff]
+  exact fun x h ↦ iInter_subset_of_subset x fun ⦃a⦄ a ↦ a
+
+theorem dissipate_antitone [Preorder α] : Antitone (Dissipate s) :=
+  fun _ _ hab ↦ biInter_subset_biInter_left fun _ hz => le_trans hz hab
+
+@[gcongr]
+theorem dissipate_subset_dissipate [Preorder α] {x y} (h : y ≤ x) :
+    Dissipate s x ⊆ Dissipate s y :=
+  dissipate_antitone h
+
+@[simp]
+theorem biInter_dissipate [Preorder α] {s : α → Set β} {x : α} :
+    Dissipate (Dissipate s) x = Dissipate s x := by
+  apply Subset.antisymm
+  · apply iInter_mono fun z y hy ↦ ?_
+    simp only [dissipate_def, mem_iInter] at *
+    exact fun h ↦ hy h z <| le_refl z
+  · simp only [subset_iInter_iff, Dissipate]
+    exact fun i hi z hz ↦ biInter_subset_of_mem <| le_trans hz hi
+
+@[simp]
+theorem iInter_dissipate [Preorder α] : ⋂ x, Dissipate s x = ⋂ x, s x := by
+  simp_rw [dissipate_def]
+  apply Subset.antisymm <;> simp_rw [subset_def, mem_iInter]
+  · exact fun z h x' ↦ h x' x' (le_refl x')
+  · exact fun z h x' y hy ↦ h y
+
+@[simp]
+lemma dissipate_bot [PartialOrder α] [OrderBot α] (s : α → Set β) : Dissipate s ⊥ = s ⊥ := by
+  simp only [dissipate_def, le_bot_iff, iInter_iInter_eq_left]
+
+open Nat
+
+@[simp]
+theorem dissipate_succ (s : ℕ → Set α) (n : ℕ) :
+    ⋂ y, ⋂ (_ : y ≤ n + 1), s y = (⋂ y, ⋂ (_ : y ≤ n), s y) ∩ s (n + 1)
+    := by
+  ext x
+  refine ⟨fun hx ↦ ?_, fun hx ↦ ?_⟩
+  · simp only [mem_inter_iff, mem_iInter, Dissipate] at *
+    exact ⟨fun i hi ↦ hx i <| le_trans hi <|
+      le_add_right n 1, hx (n + 1) <| le_refl (n + 1)⟩
+  · simp only [Dissipate, mem_inter_iff, mem_iInter] at *
+    intro i hi
+    by_cases h : i ≤ n
+    · exact hx.1 i h
+    · simp only [not_le] at h
+      exact le_antisymm hi h ▸ hx.2
+
+lemma dissipate_zero (s : ℕ → Set β) : Dissipate s 0 = s 0 := by
+  simp [dissipate_def]
+
+lemma exists_subset_dissipate_of_directed {s : ℕ → Set α}
+  (hd : Directed (fun (x1 x2 : Set α) => x2 ⊆ x1) s) (n : ℕ) : ∃ m, s m ⊆ Dissipate s n := by
+  induction n with
+  | zero => use 0; simp [dissipate_def]
+  | succ n hn =>
+    obtain ⟨m, hm⟩ := hn
+    simp_rw [dissipate_def, dissipate_succ]
+    obtain ⟨k, hk⟩ := hd m (n+1)
+    simp at hk
+    use k
+    simp only [subset_inter_iff]
+    exact ⟨le_trans hk.1 hm, hk.2⟩
+
+lemma exists_dissipate_eq_empty_iff {s : ℕ → Set α}
+    (hd : Directed (fun (x1 x2 : Set α) => x2 ⊆ x1) s) :
+      (∃ n, Dissipate s n = ∅) ↔ (∃ n, s n = ∅) := by
+  refine ⟨?_, fun ⟨n, hn⟩ ↦ ⟨n, ?_⟩⟩
+  · rw [← not_imp_not]
+    push_neg
+    intro h n
+    obtain ⟨m, hm⟩ := exists_subset_dissipate_of_directed hd n
+    exact Set.Nonempty.mono hm (h m)
+  · by_cases hn' : n = 0
+    · rw [hn']
+      exact Eq.trans (dissipate_zero s) (hn' ▸ hn)
+    · obtain ⟨k, hk⟩ := exists_eq_add_one_of_ne_zero hn'
+      rw [hk, dissipate_def, dissipate_succ, ← hk, hn, Set.inter_empty]
+
+lemma directed_dissipate {s : ℕ → Set α} :
+    Directed (fun (x1 x2 : Set α) => x2 ⊆ x1) (Dissipate s) :=
+     dissipate_antitone.directed_ge
+
+lemma exists_dissipate_eq_empty_iff_of_directed (C : ℕ → Set α)
+    (hd : Directed (fun (x1 x2 : Set α) => x2 ⊆ x1) C) :
+    (∃ n, C n = ∅) ↔ (∃ n, Dissipate C n = ∅) := by
+  refine ⟨fun ⟨n, hn⟩ ↦ ⟨n, ?_⟩ , ?_⟩
+  · by_cases hn' : n = 0
+    · rw [hn', dissipate_zero]
+      exact hn' ▸ hn
+    · obtain ⟨k, hk⟩ := exists_eq_succ_of_ne_zero hn'
+      simp_rw [hk, succ_eq_add_one, dissipate_def, dissipate_succ,
+        ← succ_eq_add_one, ← hk, hn, Set.inter_empty]
+  · rw [← not_imp_not]
+    push_neg
+    intro h n
+    obtain ⟨m, hm⟩ := exists_subset_dissipate_of_directed hd n
+    exact Set.Nonempty.mono hm (h m)
+
+/-- For a ∩-stable attribute `p` on `Set α` and a sequence of sets `s` with this attribute,
+`p (Dissipate s n)` holds. -/
+lemma dissipate_of_piSystem {s : ℕ → Set α} {p : Set α → Prop}
+    (hp : IsPiSystem p) (h : ∀ n, p (s n)) (n : ℕ) (h' : (Dissipate s n).Nonempty) :
+      p (Dissipate s n) := by
+  induction n with
+  | zero =>
+    simp only [dissipate_def, le_zero_eq, iInter_iInter_eq_left]
+    exact h 0
+  | succ n hn =>
+    rw [dissipate_def, dissipate_succ] at *
+    apply hp (Dissipate s n) (hn (Nonempty.left h')) (s (n+1)) (h (n+1)) h'
+
+end Set
diff --git a/Mathlib/MeasureTheory/PiSystem.lean b/Mathlib/MeasureTheory/PiSystem.lean
index cb23303e80d3ad..c6bc04867088c5 100644
--- a/Mathlib/MeasureTheory/PiSystem.lean
+++ b/Mathlib/MeasureTheory/PiSystem.lean
@@ -97,6 +97,14 @@ theorem IsPiSystem.insert_univ {S : Set (Set α)} (h_pi : IsPiSystem S) :
     · simp [hs, ht]
     · exact Set.mem_insert_of_mem _ (h_pi s hs t ht hst)
 
+lemma IsPiSystem.iff_of_empty_mem (S : Set (Set α)) (hS : ∅ ∈ S) :
+    (IsPiSystem S) ↔ (∀ s ∈ S, ∀ t ∈ S, s ∩ t ∈ S) := by
+  refine ⟨fun h s hs t ht ↦ ?_, fun h s hs t ht _ ↦ h s hs t ht⟩
+  by_cases h' : (s ∩ t).Nonempty
+  · exact h s hs t ht h'
+  · push_neg at h'
+    exact h' ▸ hS
+
 theorem IsPiSystem.comap {α β} {S : Set (Set β)} (h_pi : IsPiSystem S) (f : α → β) :
     IsPiSystem { s : Set α | ∃ t ∈ S, f ⁻¹' t = s } := by
   rintro _ ⟨s, hs_mem, rfl⟩ _ ⟨t, ht_mem, rfl⟩ hst
diff --git a/Mathlib/Topology/Compactness/CompactSystem.lean b/Mathlib/Topology/Compactness/CompactSystem.lean
new file mode 100644
index 00000000000000..dd520e7a1026e4
--- /dev/null
+++ b/Mathlib/Topology/Compactness/CompactSystem.lean
@@ -0,0 +1,280 @@
+/-
+Copyright (c) 2025 Peter Pfaffelhuber. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Rémy Degenne, Peter Pfaffelhuber
+-/
+import Mathlib.Data.Set.Dissipate
+import Mathlib.Topology.Separation.Hausdorff
+
+/-!
+# Compact systems.
+
+This file defines compact systems of sets.
+
+## Main definitions
+
+* `IsCompactSystem`: A set of sets is a compact system if, whenever a countable subfamily has empty
+  intersection, then finitely many of them already have empty intersection.
+
+## Main results
+
+* `IsCompactSystemiff_isCompactSystem_of_or_univ`: A set system is a compact
+system iff inserting `univ` gives a compact system.
+* `IsClosedCompact.isCompactSystem`: The set of closed and compact sets is a compact system.
+* `IsClosedCompact.isCompactSystem_of_T2Space`: In a `T2Space α`, the set of compact sets
+  is a compact system in a `T2Space`.
+-/
+
+open Set Finset Nat
+
+variable {α : Type*} {p : Set α → Prop} {C : ℕ → Set α}
+
+section definition
+
+/-- A set of sets is a compact system if, whenever a countable subfamily has empty intersection,
+then finitely many of them already have empty intersection. -/
+def IsCompactSystem (p : Set α → Prop) : Prop :=
+  ∀ C : ℕ → Set α, (∀ i, p (C i)) → ⋂ i, C i = ∅ → ∃ (n : ℕ), Dissipate C n = ∅
+
+end definition
+
+namespace IsCompactSystem
+
+open Classical in
+/-- In a compact system, given a countable family with `⋂ i, C i = ∅`, we choose the smallest `n`
+with `⋂ (i ≤ n), C i = ∅`. -/
+noncomputable
+def finite_of_empty (hp : IsCompactSystem p) (hC : ∀ i, p (C i))
+    (hC_empty : ⋂ i, C i = ∅) : ℕ :=
+  Nat.find (hp C hC hC_empty)
+
+open Classical in
+lemma dissipate_eq_empty (hp : IsCompactSystem p) (hC : ∀ i, p (C i))
+    (hC_empty : ⋂ i, C i = ∅) :
+    Dissipate C (hp.finite_of_empty hC hC_empty) = ∅ := by
+  apply Nat.find_spec (hp C hC hC_empty)
+
+theorem iff_nonempty_iInter (p : Set α → Prop) :
+    IsCompactSystem p ↔ (∀ C : ℕ → Set α, (∀ i, p (C i)) → (∀ (n : ℕ),
+      (Dissipate C n).Nonempty) → (⋂ i, C i).Nonempty) := by
+  refine ⟨fun h C hC hn ↦ ?_, fun h C hC ↦ ?_⟩ <;> have h2 := not_imp_not.mpr <| h C hC
+  · push_neg at h2
+    exact h2 hn
+  · push_neg at h2
+    exact h2
+
+/-- In this equivalent formulation for a compact system,
+note that we use `⋂ k < n, C k` rather than `⋂ k ≤ n, C k`. -/
+lemma iff_nonempty_iInter_of_lt (p : Set α → Prop) : IsCompactSystem p ↔
+    ∀ C : ℕ → Set α, (∀ i, p (C i)) → (∀ n, (⋂ k < n, C k).Nonempty) → (⋂ i, C i).Nonempty := by
+  simp_rw [iff_nonempty_iInter]
+  refine ⟨fun h C hi h'↦ ?_, fun h C hi h' ↦ ?_⟩
+  · apply h C hi
+    exact fun n ↦ dissipate_eq ▸ (h' (n + 1))
+  · apply h C hi
+    intro n
+    simp_rw [Set.nonempty_iff_ne_empty] at h' ⊢
+    intro g
+    apply h' n
+    simp_rw [← subset_empty_iff, Dissipate] at g ⊢
+    apply le_trans _ g
+    intro x
+    rw [mem_iInter₂, mem_iInter₂]
+    exact fun h i hi ↦ h i hi.le
+
+/-- Any subset of a compact system is a compact system. -/
+theorem mono {C D : (Set α) → Prop} (hD : IsCompactSystem D) (hCD : ∀ s, C s → D s) :
+  IsCompactSystem C := fun s hC hs ↦ hD s (fun i ↦ hCD (s i) (hC i)) hs
+
+/-- A set system is a compact system iff adding `∅` gives a compact system. -/
+lemma iff_isCompactSystem_of_or_empty : IsCompactSystem p ↔
+    IsCompactSystem (fun s ↦ (p s ∨ (s = ∅))) := by
+  refine ⟨fun h s h' hd ↦ ?_, fun h ↦ mono h (fun s ↦ fun a ↦ Or.symm (Or.inr a))⟩
+  by_cases g : ∃ n, s n = ∅
+  · use g.choose
+    rw [← subset_empty_iff] at hd ⊢
+    exact le_trans (dissipate_subset (by rfl)) g.choose_spec.le
+  · push_neg at g
+    have hj (i : _) : p (s i) := by
+      rcases h' i with a | b
+      · exact a
+      · exfalso
+        revert g i
+        simp_rw [← Set.not_nonempty_iff_eq_empty]
+        simp_rw [imp_false, not_not]
+        exact fun h i ↦ h i
+    exact h s hj hd
+
+lemma of_IsEmpty (h : IsEmpty α) (p : Set α → Prop) : IsCompactSystem p :=
+  fun s _ _ ↦ ⟨0, Set.eq_empty_of_isEmpty (Dissipate s 0)⟩
+
+/-- A set system is a compact system iff adding `univ` gives a compact system. -/
+lemma iff_isCompactSystem_of_or_univ : IsCompactSystem p ↔
+    IsCompactSystem (fun s ↦ (p s ∨ s = univ)) := by
+  refine ⟨fun h ↦ ?_, fun h ↦ mono h (fun s ↦ fun a ↦ Or.symm (Or.inr a))⟩
+  wlog ht : Nonempty α
+  · rw [not_nonempty_iff] at ht
+    apply of_IsEmpty ht
+  · rw [iff_nonempty_iInter] at h ⊢
+    intro s h' hd
+    classical
+    by_cases h₀ : ∀ n, ¬p (s n)
+    · simp only [h₀, false_or] at h'
+      simp_rw [h', iInter_univ, Set.univ_nonempty]
+    · push_neg at h₀
+      let n := Nat.find h₀
+      let s' := fun i ↦ if p (s i) then s i else s n
+      have h₁ : ∀ i, p (s' i) := by
+        intro i
+        by_cases h₁ : p (s i)
+        · simp only [h₁, ↓reduceIte, s']
+        · simp only [h₁, ↓reduceIte, Nat.find_spec h₀, s', n]
+      have h₃ : ∀ i, (p (s i) → s' i = s i) := fun i h ↦ if_pos h
+      have h₄ : ∀ i, (¬p (s i) → s' i = s n) := fun i h ↦ if_neg h
+      have h₂ : ⋂ i, s i = ⋂ i, s' i := by
+        simp only [s'] at *
+        ext x
+        simp only [mem_iInter]
+        refine ⟨fun h i ↦ ?_, fun h i ↦ ?_⟩
+        · by_cases h' : p (s i) <;> simp only [h', ↓reduceIte, h, s', n]
+        · specialize h' i
+          specialize h i
+          rcases h' with a | b
+          · simp only [a, ↓reduceIte, s', n] at h
+            exact h
+          · simp only [b, Set.mem_univ]
+      apply h₂ ▸ h s' h₁
+      by_contra! a
+      obtain ⟨j, hj⟩ := a
+      have h₂ (v : ℕ) (hv : n ≤ v) : Dissipate s v = Dissipate s' v:= by
+        ext x
+        refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩ <;> simp only [dissipate_def, mem_iInter] at h ⊢ <;>
+          intro i hi
+        · by_cases h₅ : p (s i)
+          · exact (h₃ i h₅) ▸ h i hi
+          · exact (h₄ i h₅) ▸ h n hv
+        · by_cases h₅ : p (s i)
+          · exact (h₃ i h₅) ▸ h i hi
+          · have h₆ : s i = univ := by
+              specialize h' i
+              simp only [h₅, false_or] at h'
+              exact h'
+            simp only [h₆, Set.mem_univ]
+      have h₇ : Dissipate s' (max j n) = ∅ := by
+        rw [← subset_empty_iff] at hj ⊢
+        exact le_trans (dissipate_antitone (Nat.le_max_left j n)) hj
+      specialize h₂ (max j n) (Nat.le_max_right j n)
+      specialize hd (max j n)
+      rw [h₂, Set.nonempty_iff_ne_empty, h₇] at hd
+      exact hd rfl
+
+theorem iff_directed (hpi : IsPiSystem p) :
+    IsCompactSystem p ↔
+    ∀ (C : ℕ → Set α), ∀ (_ : Directed (fun (x1 x2 : Set α) => x1 ⊇ x2) C), (∀ i, p (C i)) →
+      ⋂ i, C i = ∅ → ∃ (n : ℕ), C n = ∅ := by
+  rw [iff_isCompactSystem_of_or_empty]
+  refine ⟨fun h ↦ fun C hdi hi ↦ ?_, fun h C h1 h2 ↦ ?_⟩
+  · rw [exists_dissipate_eq_empty_iff_of_directed C hdi]
+    apply h C
+    exact fun i ↦ Or.inl (hi i)
+  · have hpi' : IsPiSystem (fun s ↦ p s ∨ s = ∅) := by
+      intro a ha b hb hab
+      rcases ha with ha₁ | ha₂
+      · rcases hb with hb₁ | hb₂
+        · left
+          exact hpi a ha₁ b hb₁ hab
+        · right
+          exact hb₂ ▸ (Set.inter_empty a)
+      · simp only [ha₂, Set.empty_inter]
+        right
+        rfl
+    rw [← biInter_le_eq_iInter] at h2
+    obtain h' := h (Dissipate C) directed_dissipate
+    have h₀ : (∀ (n : ℕ), p (Dissipate C n) ∨ Dissipate C n = ∅) → ⋂ n, Dissipate C n = ∅ →
+      ∃ n, Dissipate C n = ∅ := by
+      intro h₀ h₁
+      by_cases f : ∀ n, p (Dissipate C n)
+      · apply h' f h₁
+      · push_neg at f
+        obtain ⟨n, hn⟩ := f
+        use n
+        specialize h₀ n
+        simp_all only [false_or]
+    obtain h'' := dissipate_of_piSystem hpi' h1
+    have h₁ :  ∀ (n : ℕ), p (Dissipate C n) ∨ Dissipate C n = ∅ := by
+      intro n
+      by_cases g : (Dissipate C n).Nonempty
+      · exact h'' n g
+      · right
+        exact Set.not_nonempty_iff_eq_empty.mp g
+    apply h₀ h₁ h2
+
+theorem iff_directed' (hpi : IsPiSystem p) :
+    IsCompactSystem p ↔
+    ∀ (C : ℕ → Set α), ∀ (_ : Directed (fun (x1 x2 : Set α) => x1 ⊇ x2) C), (∀ i, p (C i)) →
+    (∀ (n : ℕ), (C n).Nonempty) → (⋂ i, C i).Nonempty  := by
+  rw [IsCompactSystem.iff_directed hpi]
+  refine ⟨fun h1 C h3 h4 ↦ ?_, fun h1 C h3 s ↦ ?_⟩ <;> rw [← not_imp_not] <;> push_neg
+  · exact h1 C h3 h4
+  · exact h1 C h3 s
+
+section IsCompactIsClosed
+
+variable {α : Type*} [TopologicalSpace α]
+
+/-- The set of compact and closed sets is a compact system. -/
+theorem of_isCompact_isClosed :
+    IsCompactSystem (fun s : Set α ↦ IsCompact s ∧ IsClosed s) := by
+  let p := fun (s : Set α) ↦ IsCompact s ∧ IsClosed s
+  have h2 : IsPiSystem p := by
+    intro s hs t ht _
+    refine ⟨IsCompact.inter_left ht.1 hs.2, IsClosed.inter hs.2 ht.2⟩
+  rw [IsCompactSystem.iff_directed' h2]
+  intro s hs h1 h2
+  let s' := fun (i : { j : ℕ | s j ≠ univ}) ↦ s i
+  have hs' : Directed (fun x1 x2 ↦ x1 ⊇ x2) s' := by
+    intro a b
+    obtain ⟨z, hz1, hz2⟩ := hs a.val b.val
+    have hz : s z ≠ univ := fun h ↦ a.prop <| eq_univ_of_subset hz1 h
+    use ⟨z, hz⟩
+  have htcl : ∀ (i : { j : ℕ | s j ≠ univ}), IsClosed (s i) :=
+    fun i ↦ (h1 i).2
+  have htco : ∀ (i : { j : ℕ | s j ≠ univ}), IsCompact (s i) :=
+    fun i ↦ (h1 i).1
+  haveI f : Nonempty α := by
+    apply Exists.nonempty _
+    · exact fun x ↦ x ∈ s 0
+    · exact h2 0
+  by_cases h : Nonempty ↑{j | s j ≠ Set.univ}
+  · have g :  (⋂ i, s' i).Nonempty → (⋂ i, s i).Nonempty := by
+      rw [Set.nonempty_iInter, Set.nonempty_iInter]
+      rintro ⟨x, hx⟩
+      use x
+      intro i
+      by_cases g : s i ≠ univ
+      · exact hx ⟨i, g⟩
+      · simp only [ne_eq, not_not, s'] at g
+        rw [g]
+        simp only [Set.mem_univ]
+    apply g <| IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed s' hs'
+      (fun j ↦ h2 j) htco htcl
+  · simp only [ne_eq, coe_setOf, nonempty_subtype, not_exists, not_not, s'] at h
+    simp [s', h]
+
+/-- The set of sets which are either compact and closed, or `univ`, is a compact system. -/
+theorem of_isCompact_isClosed_or_univ :
+    IsCompactSystem (fun s : Set α ↦ (IsCompact s ∧ IsClosed s) ∨ (s = univ)) := by
+  rw [← iff_isCompactSystem_of_or_univ]
+  exact of_isCompact_isClosed
+
+/-- In a `T2Space` the set of compact sets is a compact system. -/
+theorem of_isCompact [T2Space α] :
+    IsCompactSystem (fun s : Set α ↦ IsCompact s) := by
+  have h : (fun s : Set α ↦ IsCompact s) = (fun s : Set α ↦ IsCompact s ∧ IsClosed s) := by
+    ext s
+    refine ⟨fun h' ↦ ⟨h', h'.isClosed⟩, fun h ↦ h.1⟩
+  exact h ▸ (of_isCompact_isClosed)
+
+end IsCompactIsClosed
+
+end IsCompactSystem