feat (Topology/Compactness/CompactSystem): closed and compact square cylinders form a compact system

Mathlib.lean

@@ -7291,6 +7291,7 @@ public import Mathlib.Topology.Compactification.OnePoint.Sphere
 public import Mathlib.Topology.Compactification.StoneCech
 public import Mathlib.Topology.Compactness.Bases
 public import Mathlib.Topology.Compactness.Compact
+public import Mathlib.Topology.Compactness.CompactSystem
 public import Mathlib.Topology.Compactness.CompactlyCoherentSpace
 public import Mathlib.Topology.Compactness.CompactlyGeneratedSpace
 public import Mathlib.Topology.Compactness.DeltaGeneratedSpace

Mathlib/Data/Set/Accumulate.lean

@@ -35,6 +35,9 @@ def accumulate [LE α] (s : α → Set β) (x : α) : Set β :=
 theorem accumulate_def [LE α] {x : α} : accumulate s x = ⋃ y ≤ x, s y :=
   rfl
 
+theorem accumulate_eq_biInter_lt {s : ℕ → Set β} {n : ℕ} : accumulate s n = ⋃ k < n + 1, s k := by
+  simp_rw [Nat.lt_add_one_iff, accumulate]
+
 @[simp]
 theorem mem_accumulate [LE α] {x : α} {z : β} : z ∈ accumulate s x ↔ ∃ y ≤ x, z ∈ s y := by
   simp_rw [accumulate_def, mem_iUnion₂, exists_prop]
@@ -82,6 +85,7 @@ theorem disjoint_accumulate [Preorder α] (hs : Pairwise (Disjoint on s)) {i j :
   rcases hx with ⟨k, hk, hx⟩
   exact disjoint_left.1 (hs (hk.trans_lt hij).ne) hx
 
+@[simp]
 theorem accumulate_succ (u : ℕ → Set α) (n : ℕ) :
     accumulate u (n + 1) = accumulate u n ∪ u (n + 1) := biUnion_le_succ u n
 
@@ -90,4 +94,28 @@ lemma partialSups_eq_accumulate (f : ℕ → Set α) :
   ext n
   simp [partialSups_eq_sup_range, accumulate, Nat.lt_succ_iff]
 
+/-- For a directed set of sets `s : ℕ → Set α` and `n : ℕ`, there exists `m : ℕ` (maybe
+larger than `n`) such that `accumulate s n ⊆ s m`. -/
+lemma exists_subset_accumulate_of_directed {s : ℕ → Set α}
+  (hd : Directed (· ⊆ ·) s) (n : ℕ) : ∃ m, accumulate s n ⊆ s m := by
+  induction n with
+  | zero => use 0; simp [accumulate_def]
+  | succ n hn =>
+    obtain ⟨m, hm⟩ := hn
+    obtain ⟨k, hk⟩ := hd m (n + 1)
+    simp at hk
+    exact ⟨k, by simp; grind⟩
+
+lemma directed_accumulate {s : ℕ → Set α} : Directed (· ⊆ ·) (accumulate s) :=
+  monotone_accumulate.directed_le
+
+lemma exists_accumulate_eq_univ_iff_of_directed {s : ℕ → Set α} (hd : Directed (· ⊆ ·) s) :
+    (∃ n, accumulate s n = univ) ↔ ∃ n, s n = univ := by
+  refine ⟨?_, fun ⟨n, hn⟩ ↦ ⟨n,
+    subset_antisymm (subset_univ _) (hn.symm.le.trans subset_accumulate)⟩⟩
+  contrapose!
+  intro h n
+  obtain ⟨m, hm⟩ := exists_subset_accumulate_of_directed hd n
+  grind
+
 end Set

Mathlib/Data/Set/Dissipate.lean

@@ -28,6 +28,9 @@ def dissipate [LE α] (s : α → Set β) (x : α) : Set β :=
 
 theorem dissipate_def [LE α] {x : α} : dissipate s x = ⋂ y ≤ x, s y := rfl
 
+theorem dissipate_eq_biInter_lt {s : ℕ → Set β} {n : ℕ} : dissipate s n = ⋂ k < n + 1, s k := by
+  simp_rw [Nat.lt_add_one_iff, dissipate]
+
 @[simp]
 theorem mem_dissipate [LE α] {x : α} {z : β} : z ∈ dissipate s x ↔ ∀ y ≤ x, z ∈ s y := by
   simp [dissipate_def]
@@ -80,4 +83,26 @@ theorem dissipate_succ (s : ℕ → Set α) (n : ℕ) :
   simp_all only [dissipate_def, mem_iInter, mem_inter_iff]
   grind
 
+/-- For a directed set of sets `s : ℕ → Set α` and `n : ℕ`, there exists `m : ℕ` (maybe
+larger than `n`) such that `s m ⊆ dissipate s n`. -/
+lemma exists_subset_dissipate_of_directed {s : ℕ → Set α}
+  (hd : Directed (· ⊇ ·) 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
+    obtain ⟨k, hk⟩ := hd m (n + 1)
+    exact ⟨k, by simp; grind⟩
+
+lemma directed_dissipate {s : ℕ → Set α} : Directed (· ⊇ ·) (dissipate s) :=
+  antitone_dissipate.directed_ge
+
+lemma exists_dissipate_eq_empty_iff_of_directed {s : ℕ → Set α} (hd : Directed (· ⊇ ·) s) :
+    (∃ n, dissipate s n = ∅) ↔ ∃ n, s n = ∅ := by
+  refine ⟨?_, fun ⟨n, hn⟩ ↦ ⟨n, subset_eq_empty (dissipate_subset le_rfl) hn⟩⟩
+  contrapose!
+  intro h n
+  obtain ⟨m, hm⟩ := exists_subset_dissipate_of_directed hd n
+  exact (h m).mono hm
+
 end Set

Mathlib/Data/Set/Prod.lean

@@ -689,6 +689,24 @@ theorem uniqueElim_preimage [Unique ι] (t : ∀ i, Set (α i)) :
 
 section Nonempty
 
+lemma pi_image_eq_of_subset {C : (i : ι) → Set (Set (α i))} (hC : ∀ i, Nonempty (C i))
+    {s₁ s₂ : Set ι} (hst : s₁ ⊆ s₂) : s₁.pi '' s₁.pi C = s₁.pi '' s₂.pi C := by
+  classical
+  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_mono' (fun _ _ _ hx ↦ hx) hst hw1
+    use w
+
 variable [∀ i, Nonempty (α i)]
 
 theorem pi_eq_empty_iff' : s.pi t = ∅ ↔ ∃ i ∈ s, t i = ∅ := by simp [pi_eq_empty_iff]

Mathlib/MeasureTheory/Constructions/Cylinders.lean

@@ -60,11 +60,37 @@
   {S | ∃ s : Finset ι, ∃ t ∈ univ.pi C, S = (s : Set ι).pi 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 [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_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]
+
+def squareCylinders_subset_of_or_univ (C : ∀ i, Set (Set (α i))) :
+    squareCylinders C ⊆ (univ.pi '' univ.pi (fun i ↦ insert univ (C i))) := by
+  classical
+  intro x hx
+  simp only [squareCylinders, mem_pi, mem_univ, forall_const, mem_setOf_eq] at hx
+  obtain ⟨s, t, ⟨ht, hx⟩⟩ := hx
+  simp only [mem_image, mem_pi, mem_univ, mem_insert_iff, forall_const]
+  use fun i ↦ (if (i ∈ s) then (t i) else univ)
+  refine ⟨?_, ?_⟩
+  · intro i
+    by_cases h : i ∈ s
+    · right
+      simp [h, ht]
+    · left
+      simp [h]
+  · exact hx ▸ univ_pi_ite s t
+
 theorem isPiSystem_squareCylinders {C : ∀ i, Set (Set (α i))} (hC : ∀ i, IsPiSystem (C i))
     (hC_univ : ∀ i, univ ∈ C i) :
     IsPiSystem (squareCylinders C) := by

Mathlib/MeasureTheory/PiSystem.lean

@@ -5,6 +5,7 @@ Authors: Johannes Hölzl, Martin Zinkevich, Rémy Degenne
 -/
 module
 
+public import Mathlib.Data.Set.Dissipate
 public import Mathlib.Logic.Encodable.Lattice
 public import Mathlib.MeasureTheory.MeasurableSpace.Defs
 public import Mathlib.Order.Disjointed
@@ -107,6 +108,17 @@ theorem IsPiSystem.comap {α β} {S : Set (Set β)} (h_pi : IsPiSystem S) (f : 
   rw [← Set.preimage_inter] at hst ⊢
   exact ⟨s ∩ t, h_pi s hs_mem t ht_mem (nonempty_of_nonempty_preimage hst), rfl⟩
 
+/-- For a `π`-system `C` over `α` and a sequence of sets `s` belonging to `C`,
+`dissipate s n` belongs to `C`. -/
+lemma IsPiSystem.dissipate_mem {s : ℕ → Set α} {C : Set (Set α)}
+    (hC : IsPiSystem C) (h : ∀ n, s n ∈ C) (n : ℕ) (h' : (dissipate s n).Nonempty) :
+    dissipate s n ∈ C := by
+  induction n with
+  | zero => simpa using h 0
+  | succ n hn =>
+    rw [dissipate_succ] at h' ⊢
+    exact hC (dissipate s n) (hn h'.left) (s (n + 1)) (h (n + 1)) h'
+
 theorem isPiSystem_iUnion_of_directed_le {α ι} (p : ι → Set (Set α))
     (hp_pi : ∀ n, IsPiSystem (p n)) (hp_directed : Directed (· ≤ ·) p) :
     IsPiSystem (⋃ n, p n) := by