feat(Topology/Compactness/CompactSystem): set system of finite unions of sets in a compact system is again a compact system

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/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
@@ -863,7 +882,30 @@ theorem subset_pi_eval_image (s : Set ι) (u : Set (∀ i, α i)) : u ⊆ pi s f
   fun f hf _ _ => ⟨f, hf, rfl⟩
 
 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
+    (pi univ fun i => if i ∈ s then t i else univ) = s.pi t := by
+  ext
+  simp_rw [mem_univ_pi]
+  refine forall_congr' fun i => ?_
+  split_ifs with h <;> simp [h]
+
+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