diff --git a/Mathlib.lean b/Mathlib.lean
index 13a9a9ff188c03..5b4751deecfa23 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -3519,6 +3519,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
@@ -6372,6 +6373,7 @@ import Mathlib.Topology.Compactification.OnePointEquiv
 import Mathlib.Topology.Compactification.StoneCech
 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..731684192a4470 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.
+
 -/
 
 
diff --git a/Mathlib/Data/Set/Dissipate.lean b/Mathlib/Data/Set/Dissipate.lean
new file mode 100644
index 00000000000000..26b987c3424f38
--- /dev/null
+++ b/Mathlib/Data/Set/Dissipate.lean
@@ -0,0 +1,158 @@
+/-
+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` is the intersection of `s y` for `y ≤ x`. -/
+def dissipate [LE α] (s : α → Set β) (x : α) : Set β :=
+  ⋂ y ≤ x, s y
+
+@[simp]
+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 iInter_subset_dissipate [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 antitone_dissipate [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 :=
+  antitone_dissipate h
+
+@[simp]
+theorem dissipate_dissipate [Preorder α] {s : α → Set β} {x : α} :
+    ⋂ y, ⋂ (_ : y ≤ x), ⋂ y_1, ⋂ (_ : y_1 ≤ y), s y_1 = ⋂ y, ⋂ (_ : y ≤ x), s y := by
+  apply Subset.antisymm
+  · apply iInter_mono fun z y hy ↦ ?_
+    simp only [mem_iInter] at *
+    exact fun h ↦ hy h z <| le_refl z
+  · simp only [subset_iInter_iff]
+    exact fun i hi z hz ↦ biInter_subset_of_mem <| le_trans hz hi
+
+@[simp]
+theorem iInter_dissipate [Preorder α] : ⋂ x, ⋂ y, ⋂ (_ : y ≤ x), s y = ⋂ x, s x := by
+  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
+
+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 : ℕ) :
+    ⋂ i, ⋂ (_ : i ≤ n + 1), s i = (dissipate s n) ∩ s (n + 1)
+    := by
+  ext x
+  simp_all only [dissipate_def, mem_iInter, mem_inter_iff]
+  refine ⟨fun a ↦ ?_, fun a i c ↦ ?_⟩
+  · simp_all only [le_refl, and_true]
+    intro i i_1
+    apply a i <| le_trans i_1 (le_succ n)
+  · obtain ⟨left, right⟩ := a
+    · by_cases h : i ≤ n
+      · exact left i h
+      · have h : i = n + 1 := by
+          simp only [not_le] at h
+          exact le_antisymm c h
+        exact h.symm ▸ right
+
+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 (x y : Set α) => y ⊆ x) s) (n : ℕ) : ∃ m, s m ⊆ dissipate s n := by
+  induction n with
+  | zero => use 0; simp
+  | 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 (x y : Set α) => y ⊆ x) 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 (x y : Set α) => y ⊆ x) (dissipate s) :=
+     antitone_dissipate.directed_ge
+
+lemma exists_dissipate_eq_empty_iff_of_directed (C : ℕ → Set α)
+    (hd : Directed (fun (x y : Set α) => y ⊆ x) 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 set of sets `p` on `α` and a sequence of sets `s` with this attribute,
+`p (dissipate s n)` holds. -/
+lemma IsPiSystem.dissipate_mem {s : ℕ → Set α} {p : Set (Set α)}
+    (hp : IsPiSystem p) (h : ∀ n, s n ∈ p) (n : ℕ) (h' : (dissipate s n).Nonempty) :
+      (dissipate s n) ∈ p := 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/Data/Set/Prod.lean b/Mathlib/Data/Set/Prod.lean
index 55aacc6e21b3a2..99b6f3f7c989ed 100644
--- a/Mathlib/Data/Set/Prod.lean
+++ b/Mathlib/Data/Set/Prod.lean
@@ -684,6 +684,21 @@ theorem pi_eq_empty_iff' : s.pi t = ∅ ↔ ∃ i ∈ s, t i = ∅ := by simp [p
 theorem disjoint_pi : Disjoint (s.pi t₁) (s.pi t₂) ↔ ∃ i ∈ s, Disjoint (t₁ i) (t₂ i) := by
   simp only [disjoint_iff_inter_eq_empty, ← pi_inter_distrib, pi_eq_empty_iff']
 
+theorem pi_nonempty_iff' [∀ i, Decidable (i ∈ s)] :
+    (s.pi t).Nonempty ↔ ∀ i ∈ s, (t i).Nonempty := by
+  classical
+  rw [pi_nonempty_iff]
+  have h := fun i ↦ exists_mem_of_nonempty (α i)
+  choose y hy using h
+  refine ⟨fun h i hi ↦ ?_, fun h i ↦ ?_⟩
+  · obtain ⟨x, hx⟩ := h i
+    exact ⟨x, hx hi⟩
+  · choose x hx using h
+    use (if g : i ∈ s then x i g else y i)
+    intro hi
+    simp only [hi, ↓reduceDIte]
+    exact hx i hi
+
 end Nonempty
 
 @[simp]
@@ -717,6 +732,10 @@ theorem pi_if {p : ι → Prop} [h : DecidablePred p] (s : Set ι) (t₁ t₂ :
 theorem union_pi : (s₁ ∪ s₂).pi t = s₁.pi t ∩ s₂.pi t := by
   simp [pi, or_imp, forall_and, setOf_and]
 
+theorem pi_antitone (h : s₁ ⊆ s₂) : s₂.pi t ⊆ s₁.pi t := by
+  rw [← union_diff_cancel h, union_pi]
+  exact Set.inter_subset_left
+
 theorem union_pi_inter
     (ht₁ : ∀ i ∉ s₁, t₁ i = univ) (ht₂ : ∀ i ∉ s₂, t₂ i = univ) :
     (s₁ ∪ s₂).pi (fun i ↦ t₁ i ∩ t₂ i) = s₁.pi t₁ ∩ s₂.pi t₂ := by
@@ -865,6 +884,25 @@ theorem subset_pi_eval_image (s : Set ι) (u : Set (∀ i, α i)) : u ⊆ pi s f
 theorem univ_pi_ite (s : Set ι) [DecidablePred (· ∈ s)] (t : ∀ i, Set (α i)) :
     (pi univ fun i => if i ∈ s then t i else univ) = s.pi t := by grind
 
+lemma pi_image_eq_of_subset {C : (i : ι) → Set (Set (α i))}
+  (hC : ∀ i, Nonempty (C i))
+  {s₁ s₂ : Set ι} [∀ i : ι, Decidable (i ∈ s₁)]
+    (hst : s₁ ⊆ s₂) : s₁.pi '' s₁.pi C = s₁.pi '' s₂.pi C := by
+  let C_mem (i : ι) : Set (α i) := ((Set.exists_mem_of_nonempty (C i)).choose : Set (α i))
+  have h_mem (i : ι) : C_mem i ∈ C i := by
+    simp [C_mem]
+  ext f
+  refine ⟨fun ⟨x, ⟨hx1, hx2⟩⟩ ↦ ?_, fun ⟨w, ⟨hw1, hw2⟩⟩ ↦ ?_⟩
+  · use fun i ↦ if i ∈ s₁ then x i else C_mem i
+    refine ⟨fun i hi ↦ ?_, ?_⟩
+    · by_cases h1 : i ∈ s₁ <;> simp only [h1, ↓reduceIte]
+      · exact hx1 i h1
+      · exact h_mem i
+    · rw [← hx2]
+      exact pi_congr rfl (fun i hi ↦ by simp only [hi, ↓reduceIte])
+  · have hw3 := pi_antitone hst hw1
+    use w
+
 end Pi
 
 end Set
diff --git a/Mathlib/MeasureTheory/Constructions/Cylinders.lean b/Mathlib/MeasureTheory/Constructions/Cylinders.lean
index 0c1e925a61b400..58ee3b4376cc82 100644
--- a/Mathlib/MeasureTheory/Constructions/Cylinders.lean
+++ b/Mathlib/MeasureTheory/Constructions/Cylinders.lean
@@ -3,9 +3,11 @@ Copyright (c) 2023 Rémy Degenne. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Rémy Degenne, Peter Pfaffelhuber, Yaël Dillies, Kin Yau James Wong
 -/
+import Mathlib.Data.Finset.Lattice.Basic
 import Mathlib.MeasureTheory.MeasurableSpace.Constructions
-import Mathlib.MeasureTheory.PiSystem
+import Mathlib.MeasureTheory.SetSemiring
 import Mathlib.Topology.Constructions
+import Mathlib.MeasureTheory.SetAlgebra
 
 /-!
 # π-systems of cylinders and square cylinders
@@ -24,6 +26,8 @@ Given a finite set `s` of indices, a cylinder is the product of a set of `∀ i
 a product set.
 
 * `cylinder s S`: cylinder with base set `S : Set (∀ i : s, α i)` where `s` is a `Finset`
+* `squareCylinder s S`: square cylinder with base set `S : (∀ i : s, Set (α i))` where
+  `s` is a `Finset`
 * `squareCylinders C` with `C : ∀ i, Set (Set (α i))`: set of all square cylinders such that for
   all `i` in the finset defining the box, the projection to `α i` belongs to `C i`. The main
   application of this is with `C i = {s : Set (α i) | MeasurableSet s}`.
@@ -48,62 +52,105 @@ variable {ι : Type _} {α : ι → Type _}
 
 section squareCylinders
 
-/-- Given a finite set `s` of indices, a square cylinder is the product of a set `S` of
-`∀ i : s, α i` and of `univ` on the other indices. The set `S` is a product of sets `t i` such that
+/-- Given a finite set `s` of indices, a square cylinder is the product of sets `t i : Set (α i)`
+for `i ∈ s` and of `univ` on the other indices. -/
+def squareCylinder (s : Finset ι) (t : ∀ i, Set (α i)) : Set (∀ i, α i) :=
+  (s : Set ι).pi t
+
+/-- The set `S` is a product of sets `t i` such that
 for all `i : s`, `t i ∈ C i`.
 `squareCylinders` is the set of all such squareCylinders. -/
 def squareCylinders (C : ∀ i, Set (Set (α i))) : Set (Set (∀ i, α i)) :=
-  {S | ∃ s : Finset ι, ∃ t ∈ univ.pi C, S = (s : Set ι).pi t}
+  {S | ∃ s : Finset ι, ∃ t ∈ univ.pi C, S = squareCylinder s t}
 
 theorem squareCylinders_eq_iUnion_image (C : ∀ i, Set (Set (α i))) :
-    squareCylinders C = ⋃ s : Finset ι, (fun t ↦ (s : Set ι).pi t) '' univ.pi C := by
+    squareCylinders C = ⋃ s : Finset ι, (s : Set ι).pi  '' univ.pi C := by
+  ext1 f
+  simp only [squareCylinder, squareCylinders, mem_iUnion, mem_image, mem_univ_pi,
+    mem_setOf_eq, eq_comm (a := f)]
+
+theorem squareCylinders_eq_iUnion_image' (C : ∀ i, Set (Set (α i))) (hC : ∀ i, Nonempty (C i)) :
+    squareCylinders C = ⋃ s : Finset ι, (s : Set ι).pi '' (s : Set ι).pi C := by
+  classical
   ext1 f
-  simp only [squareCylinders, mem_iUnion, mem_image, mem_univ_pi, mem_setOf_eq,
-    eq_comm (a := f)]
+  simp only [squareCylinder, squareCylinders, mem_iUnion, mem_image, mem_setOf_eq, eq_comm (a := f)]
+  have h (s : Set ι): s.pi '' s.pi C = s.pi '' univ.pi C := by
+    refine pi_image_eq_of_subset hC (subset_univ s)
+  simp_rw [← mem_image, h]
 
-theorem isPiSystem_squareCylinders {C : ∀ i, Set (Set (α i))} (hC : ∀ i, IsPiSystem (C i))
-    (hC_univ : ∀ i, univ ∈ C i) :
-    IsPiSystem (squareCylinders C) := by
-  rintro S₁ ⟨s₁, t₁, h₁, rfl⟩ S₂ ⟨s₂, t₂, h₂, rfl⟩ hst_nonempty
+@[simp]
+theorem mem_squareCylinders (C : ∀ i, Set (Set (α i))) (hC : ∀ i, Nonempty (C i)) (S : _) :
+    S ∈ squareCylinders C ↔ ∃ (s t : _) (_ : ∀ i ∈ s, t i ∈ C i), S = squareCylinder s t := by
+  simp_rw [squareCylinders_eq_iUnion_image, squareCylinder]
+  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
+  · simp only [mem_iUnion, mem_image, mem_pi, mem_univ, forall_const] at h
+    obtain ⟨s, t, h₀, h₁⟩ := h
+    use s, t
+    simp only [h₁, h₀, implies_true, exists_const]
+  · obtain ⟨s, t, h₀, rfl⟩ := h
+    simp only [mem_iUnion, mem_image, mem_pi, mem_univ, forall_const]
+    classical
+    use s, (fun i ↦ if i ∈ s.toSet then t i else (hC i).some)
+    refine ⟨fun i ↦ ?_ ,?_⟩
+    · by_cases h : i ∈ s <;> simp only [Finset.mem_coe, h, ↓reduceIte, Subtype.coe_prop, h₀]
+    · refine Set.pi_congr rfl (fun i hi ↦ by simp only [hi, ↓reduceIte] at *)
+
+theorem squareCylinders_subset_pi (C : ∀ i, Set (Set (α i))) (hC : ∀ i, univ ∈ C i) :
+    squareCylinders C ⊆ univ.pi '' univ.pi C := by
+  intro S hS
+  obtain ⟨s, t, h₀, h₁⟩ := hS
+  simp only [squareCylinder, mem_pi, mem_univ, forall_const] at h₀ h₁
+  classical
+  use fun i ↦ (if i ∈ s.toSet then (t i) else univ)
+  refine ⟨fun i ↦ ?_, ?_⟩
+  · simp only [mem_univ, forall_const]
+    by_cases hi : i ∈ s.toSet <;> simp only [hi, ↓reduceIte]
+    · exact h₀ i
+    · exact hC i
+  · rw [h₁, univ_pi_ite s t]
+
+theorem isPiSystem_squareCylinders [∀ i, Inhabited (α i)] {C : ∀ i, Set (Set (α i))}
+    (hC : ∀ i, IsPiSystem (C i)) (hC_univ : ∀ i, univ ∈ C i) : IsPiSystem (squareCylinders C) := by
   classical
+  haveI h_nempty : ∀ i, Nonempty (C i) := fun i ↦ Nonempty.intro ⟨Set.univ, hC_univ i⟩
+  rintro S₁ ⟨s₁, t₁, h₁, rfl⟩ S₂ ⟨s₂, t₂, h₂, rfl⟩  hst_nonempty
   let t₁' := s₁.piecewise t₁ (fun i ↦ univ)
+  simp only [Set.mem_pi, Set.mem_univ, forall_const] at h₁ h₂
+  have ht₁ (i : ι) : t₁' i ∈ C i := by
+    by_cases h : i ∈ s₁
+    · simp only [h, Finset.piecewise_eq_of_mem, t₁']
+      exact h₁ i
+    · simp only [t₁']
+      rw [Finset.piecewise_eq_of_notMem s₁ t₁ (fun i ↦ univ) h]
+      exact hC_univ i
   let t₂' := s₂.piecewise t₂ (fun i ↦ univ)
-  have h1 : ∀ i ∈ (s₁ : Set ι), t₁ i = t₁' i :=
-    fun i hi ↦ (Finset.piecewise_eq_of_mem _ _ _ hi).symm
-  have h1' : ∀ i ∉ (s₁ : Set ι), t₁' i = univ :=
-    fun i hi ↦ Finset.piecewise_eq_of_notMem _ _ _ hi
-  have h2 : ∀ i ∈ (s₂ : Set ι), t₂ i = t₂' i :=
-    fun i hi ↦ (Finset.piecewise_eq_of_mem _ _ _ hi).symm
-  have h2' : ∀ i ∉ (s₂ : Set ι), t₂' i = univ :=
-    fun i hi ↦ Finset.piecewise_eq_of_notMem _ _ _ hi
-  rw [Set.pi_congr rfl h1, Set.pi_congr rfl h2, ← union_pi_inter h1' h2']
-  refine ⟨s₁ ∪ s₂, fun i ↦ t₁' i ∩ t₂' i, ?_, ?_⟩
-  · rw [mem_univ_pi]
-    intro i
-    have : (t₁' i ∩ t₂' i).Nonempty := by
-      obtain ⟨f, hf⟩ := hst_nonempty
-      rw [Set.pi_congr rfl h1, Set.pi_congr rfl h2, mem_inter_iff, mem_pi, mem_pi] at hf
-      refine ⟨f i, ⟨?_, ?_⟩⟩
-      · by_cases hi₁ : i ∈ s₁
-        · exact hf.1 i hi₁
-        · rw [h1' i hi₁]
-          exact mem_univ _
-      · by_cases hi₂ : i ∈ s₂
-        · exact hf.2 i hi₂
-        · rw [h2' i hi₂]
-          exact mem_univ _
-    refine hC i _ ?_ _ ?_ this
-    · by_cases hi₁ : i ∈ s₁
-      · rw [← h1 i hi₁]
-        exact h₁ i (mem_univ _)
-      · rw [h1' i hi₁]
-        exact hC_univ i
-    · by_cases hi₂ : i ∈ s₂
-      · rw [← h2 i hi₂]
-        exact h₂ i (mem_univ _)
-      · rw [h2' i hi₂]
-        exact hC_univ i
-  · rw [Finset.coe_union]
+  have ht₂ (i : ι) : t₂' i ∈ C i := by
+    by_cases h : i ∈ s₂
+    · simp only [h, Finset.piecewise_eq_of_mem, t₂']
+      exact h₂ i
+    · simp only [t₂']
+      rw [Finset.piecewise_eq_of_notMem s₂ t₂ (fun i ↦ univ) h]
+      exact hC_univ i
+  have h₁ : (s₁ : Set ι).pi t₁' = (s₁ : Set ι).pi t₁ := by
+    refine Set.pi_congr rfl ?_
+    exact fun i a ↦ (s₁.piecewise_eq_of_mem t₁ (fun i ↦ Set.univ) a)
+  have h₂ : (s₂ : Set ι).pi t₂' = (s₂ : Set ι).pi t₂ := by
+    refine Set.pi_congr rfl ?_
+    exact fun i a ↦ (s₂.piecewise_eq_of_mem t₂ (fun i ↦ Set.univ) a)
+  have h : squareCylinder s₁ t₁ ∩ squareCylinder s₂ t₂ = squareCylinder (s₁ ∪ s₂)
+      (fun i ↦ t₁' i ∩ t₂' i) := by
+    rw [squareCylinder, squareCylinder, squareCylinder, Finset.coe_union, union_pi_inter, h₁, h₂]
+      <;>
+    exact fun i a ↦ Finset.piecewise_eq_of_notMem _ _ (fun i ↦ Set.univ) a
+  rw [h] at hst_nonempty ⊢
+  rw [squareCylinder, squareCylinders_eq_iUnion_image' C, mem_iUnion]
+  · use (s₁ ∪ s₂), (fun i ↦ t₁' i ∩ t₂' i)
+    refine ⟨?_, rfl⟩
+    apply fun i _ ↦ hC i (t₁' i) (ht₁ i) (t₂' i) (ht₂ i) _
+    intro i hi
+    rw [squareCylinder, pi_nonempty_iff'] at hst_nonempty
+    exact hst_nonempty i hi
+  · assumption
 
 theorem comap_eval_le_generateFrom_squareCylinders_singleton
     (α : ι → Type*) [m : ∀ i, MeasurableSpace (α i)] (i : ι) :
@@ -124,7 +171,7 @@ theorem comap_eval_le_generateFrom_squareCylinders_singleton
     · simp only [hji, not_false_iff, dif_neg, MeasurableSet.univ]
   · simp only [eq_mpr_eq_cast, ← h]
     ext1 x
-    simp only [Function.eval, cast_eq, dite_eq_ite, ite_true, mem_preimage]
+    simp only [Function.eval, cast_eq, dite_eq_ite, ite_true, Set.mem_preimage]
 
 /-- The square cylinders formed from measurable sets generate the product σ-algebra. -/
 theorem generateFrom_squareCylinders [∀ i, MeasurableSpace (α i)] :
@@ -349,6 +396,33 @@ theorem diff_mem_measurableCylinders (hs : s ∈ measurableCylinders α)
   rw [diff_eq_compl_inter]
   exact inter_mem_measurableCylinders (compl_mem_measurableCylinders ht) hs
 
+
+section MeasurableCylinders
+
+lemma isSetAlgebra_measurableCylinders : IsSetAlgebra (measurableCylinders α) where
+  empty_mem := empty_mem_measurableCylinders α
+  compl_mem _ := compl_mem_measurableCylinders
+  union_mem _ _ := union_mem_measurableCylinders
+
+lemma isSetRing_measurableCylinders : IsSetRing (measurableCylinders α) :=
+  isSetAlgebra_measurableCylinders.isSetRing
+
+lemma isSetSemiring_measurableCylinders : MeasureTheory.IsSetSemiring (measurableCylinders α) :=
+  isSetRing_measurableCylinders.isSetSemiring
+
+end MeasurableCylinders
+
+
+theorem iUnion_le_mem_measurableCylinders {s : ℕ → Set (∀ i : ι, α i)}
+    (hs : ∀ n, s n ∈ measurableCylinders α) (n : ℕ) :
+    (⋃ i ≤ n, s i) ∈ measurableCylinders α :=
+  isSetRing_measurableCylinders.iUnion_le_mem hs n
+
+theorem iInter_le_mem_measurableCylinders {s : ℕ → Set (∀ i : ι, α i)}
+    (hs : ∀ n, s n ∈ measurableCylinders α) (n : ℕ) :
+    (⋂ i ≤ n, s i) ∈ measurableCylinders α :=
+  isSetRing_measurableCylinders.iInter_le_mem hs n
+
 /-- The measurable cylinders generate the product σ-algebra. -/
 theorem generateFrom_measurableCylinders :
     MeasurableSpace.generateFrom (measurableCylinders α) = MeasurableSpace.pi := by
@@ -457,4 +531,5 @@ lemma measurable_restrict_cylinderEvents (Δ : Set ι) :
   rw [@measurable_pi_iff]; exact fun i ↦ measurable_cylinderEvent_apply i.2
 
 end cylinderEvents
+
 end MeasureTheory
diff --git a/Mathlib/MeasureTheory/Constructions/ProjectiveFamilyContent.lean b/Mathlib/MeasureTheory/Constructions/ProjectiveFamilyContent.lean
index d198a0f5f15ae4..c424fbb7fb7855 100644
--- a/Mathlib/MeasureTheory/Constructions/ProjectiveFamilyContent.lean
+++ b/Mathlib/MeasureTheory/Constructions/ProjectiveFamilyContent.lean
@@ -5,7 +5,6 @@ Authors: Rémy Degenne, Peter Pfaffelhuber
 -/
 import Mathlib.MeasureTheory.Constructions.Projective
 import Mathlib.MeasureTheory.Measure.AddContent
-import Mathlib.MeasureTheory.SetAlgebra
 
 /-!
 # Additive content built from a projective family of measures
@@ -43,21 +42,6 @@ variable {ι : Type*} {α : ι → Type*} {mα : ∀ i, MeasurableSpace (α i)}
   {P : ∀ J : Finset ι, Measure (Π j : J, α j)} {s t : Set (Π i, α i)} {I : Finset ι}
   {S : Set (Π i : I, α i)}
 
-section MeasurableCylinders
-
-lemma isSetAlgebra_measurableCylinders : IsSetAlgebra (measurableCylinders α) where
-  empty_mem := empty_mem_measurableCylinders α
-  compl_mem _ := compl_mem_measurableCylinders
-  union_mem _ _ := union_mem_measurableCylinders
-
-lemma isSetRing_measurableCylinders : IsSetRing (measurableCylinders α) :=
-  isSetAlgebra_measurableCylinders.isSetRing
-
-lemma isSetSemiring_measurableCylinders : MeasureTheory.IsSetSemiring (measurableCylinders α) :=
-  isSetRing_measurableCylinders.isSetSemiring
-
-end MeasurableCylinders
-
 section ProjectiveFamilyFun
 
 open Classical in
diff --git a/Mathlib/MeasureTheory/PiSystem.lean b/Mathlib/MeasureTheory/PiSystem.lean
index 92cc30b6405765..9857d76bf11e31 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..652006cdab7fd8
--- /dev/null
+++ b/Mathlib/Topology/Compactness/CompactSystem.lean
@@ -0,0 +1,382 @@
+/-
+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.Logic.IsEmpty
+import Mathlib.MeasureTheory.Constructions.Cylinders
+import Mathlib.Order.OmegaCompletePartialOrder
+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`.
+* `IsCompactSystem.closedCompactSquareCylinders`: Closed and compact square cylinders form a
+  compact system.
+-/
+
+open Set Nat MeasureTheory
+
+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, n]
+        · specialize h' i
+          specialize h i
+          rcases h' with a | b
+          · simp only [a, ↓reduceIte] 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 (antitone_dissipate (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'' := IsPiSystem.dissipate_mem 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] 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] at h
+    simp [h]
+
+theorem nonempty_isCompactIsClosed : Nonempty { t : Set α | IsCompact t ∧ IsClosed t } := by
+  simp only [coe_setOf, nonempty_subtype]
+  use ∅
+  simp
+
+/-- 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
+
+
+section pi
+
+variable {ι : Type*} {α : ι → Type*}
+
+/- In a product space, the intersection of square cylinders is empty iff there is a coordinate `i`
+such that the projections to `i` have empty intersection. -/
+theorem iInter_pi_empty_iff {β : Type*} (s : β → Set ι) (t : β → (i : ι) → Set (α i)) :
+   (⋂ b, ((s b).pi (t b)) = ∅) ↔ (∃ i : ι, ⋂ (b : β) (_: i ∈ s b), (t b i) = ∅):= by
+  rw [iInter_eq_empty_iff, not_iff_not.symm]
+  push_neg
+  simp only [nonempty_iInter, mem_iInter]
+  refine ⟨fun ⟨x, hx⟩ i ↦ ?_, fun h ↦ ?_⟩
+  · refine ⟨x i, fun j hi ↦ hx j i hi⟩
+  · choose x hx using h
+    refine ⟨x, fun i j hj ↦ hx j i hj⟩
+
+theorem iInter_univ_pi_empty_iff {β : Type*} (t : β → (i : ι) → Set (α i)) :
+   ( ⋂ b, (univ.pi (t b)) = ∅) ↔ (∃ i : ι, ⋂ (b : β), (t b i) = ∅):= by
+  rw [iInter_pi_empty_iff]
+  simp only [mem_univ, iInter_true]
+
+theorem biInter_univ_pi_empty_iff {β : Type*} (t : β → (i : ι) → Set (α i)) (p : β → Prop) :
+   ( ⋂ (b : β), ⋂ (_ : p b), (univ.pi (t b)) = ∅) ↔
+      (∃ i : ι, ⋂ (b : β), ⋂ (_ : p b), (t b i) = ∅) := by
+  have h :  ⋂ (b : β), ⋂ (_ : p b), (univ.pi (t b)) =
+      ⋂ (b : { (b' : β) | p b' }), (univ.pi (t b.val)) := by
+    exact biInter_eq_iInter p fun x h ↦ univ.pi (t x)
+  have h' (i : ι) :  ⋂ (b : β), ⋂ (_ : p b), t b i =  ⋂ (b : { (b' : β) | p b' }), t b.val i := by
+    exact biInter_eq_iInter p fun x h ↦ t x i
+  simp_rw [h, h', iInter_univ_pi_empty_iff]
+
+theorem pi (C : (i : ι) → Set (Set (α i))) (hC : ∀ i, IsCompactSystem (C i)) :
+    IsCompactSystem (univ.pi '' univ.pi C) := by
+  intro S hS h_empty
+  change ∀ i, S i ∈ univ.pi '' univ.pi C at hS
+  simp only [mem_image, mem_pi, mem_univ, forall_const] at hS
+  choose x hx1 hx2 using hS
+  simp_rw [← hx2] at h_empty ⊢
+  simp_rw [iInter_univ_pi_empty_iff x] at h_empty
+  obtain ⟨i, hi⟩ := h_empty
+  let y := (fun b ↦ x b i)
+  have hy (b : ℕ) : y b ∈ C i := by
+    simp only [y]
+    exact hx1 b i
+  have ⟨n, hn⟩ := (hC i) y hy hi
+  use n
+  simp_rw [dissipate, ← hx2] at hn ⊢
+  rw [biInter_univ_pi_empty_iff x]
+  use i
+
+theorem squareCylinders (C : (i : ι) → Set (Set (α i))) (hC₀ : ∀ i, IsCompactSystem (C i))
+    (hC₁ : ∀ i, Nonempty (C i)) :
+    IsCompactSystem (squareCylinders C) := by
+  apply IsCompactSystem.mono (pi _ (fun i ↦ iff_isCompactSystem_of_or_univ.mp (hC₀  i)))
+  intro S hS
+  apply squareCylinders_subset_pi _ (fun i ↦ Or.inr rfl)
+  change S ∈ MeasureTheory.squareCylinders C at hS
+  rw [mem_squareCylinders C hC₁] at hS
+  rw [mem_squareCylinders (fun i s ↦ C i s ∨ s = univ)
+    (fun i ↦ nonempty_subtype.mpr ⟨univ, Or.inr rfl⟩)]
+  obtain ⟨s, t, h₀, h₁⟩ := hS
+  use s, t
+  simp only [exists_prop]
+  exact ⟨fun i hi ↦ Or.inl (h₀ i hi), h₁⟩
+
+end pi
+
+end IsCompactSystem
+
+section ClosedCompactSquareCylinders
+
+variable {ι : Type*} {α : ι → Type*}
+
+variable [∀ i, TopologicalSpace (α i)]
+
+variable (α)
+/-- The set of sets of the form `s.pi t`, where `s : Finset ι` and `t i` is both,
+closed and compact, for all `i ∈ s`. -/
+def MeasureTheory.compactClosedSquareCylinders : Set (Set (Π i, α i)) :=
+  MeasureTheory.squareCylinders (fun i ↦ { t : Set (α i) | IsCompact t ∧ IsClosed t })
+
+/-- Products of compact and closed sets form a a compact system. -/
+theorem IsCompactSystem.compactClosedPi :
+    IsCompactSystem (univ.pi '' univ.pi (fun i ↦ { t : Set (α i) | IsCompact t ∧ IsClosed t })) :=
+  IsCompactSystem.pi _ (fun _ ↦ IsCompactSystem.of_isCompact_isClosed)
+
+/-- Compact and closed square cylinders are a compact system. -/
+theorem isCompactSystem.compactClosedSquareCylinders :
+    IsCompactSystem (MeasureTheory.compactClosedSquareCylinders α) :=
+  IsCompactSystem.squareCylinders _ (fun _ ↦ IsCompactSystem.of_isCompact_isClosed)
+    (fun _ ↦ IsCompactSystem.nonempty_isCompactIsClosed)
+
+end ClosedCompactSquareCylinders