feat(Topology/Compactness/CompactSystem): introduce compact Systems

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

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.
+
 -/
 
 

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

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