[Merged by Bors] - feat(Topology/Compactness/CompactSystem): introduce compact Systems

Mathlib.lean

@@ -7264,6 +7264,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/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_iInter_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,27 @@ 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 (fun (x y : Set α) => y ⊆ x) 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 (fun x y ↦ y ⊆ x) (dissipate s) :=
+  antitone_dissipate.directed_ge
+
+lemma exists_dissipate_eq_empty_iff_of_directed (C : ℕ → Set α)
+    (hd : Directed (fun x y ↦ y ⊆ x) C) :
+    (∃ n, C n = ∅) ↔ (∃ n, dissipate C 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/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 ∩-stable set of sets `C` on `α` and a sequence of sets `s` with this attribute,
+`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

Mathlib/Topology/Compactness/CompactSystem.lean

@@ -0,0 +1,199 @@
+/-
+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
+-/
+module
+
+public import Mathlib.MeasureTheory.PiSystem
+public 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
+
+* `isCompactSystem_insert_univ_iff`: A set system is a compact system iff inserting `univ`
+  gives a compact system.
+* `isCompactSystem_isCompact_isClosed`: The set of closed and compact sets is a compact system.
+* `isCompactSystem_isCompact`: In a `T2Space`, the set of compact sets is a compact system.
+-/
+
+@[expose] public section
+
+open Set Finset Nat
+
+variable {α : Type*} {S : Set (Set α)} {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 (S : Set (Set α)) : Prop :=
+  ∀ C : ℕ → Set α, (∀ i, C i ∈ S) → ⋂ i, C i = ∅ → ∃ (n : ℕ), dissipate C n = ∅
+
+end definition
+
+namespace IsCompactSystem
+
+lemma of_nonempty_iInter
+    (h : ∀ C : ℕ → Set α, (∀ i, C i ∈ S) → (∀ n, (dissipate C n).Nonempty) → (⋂ i, C i).Nonempty) :
+    IsCompactSystem S := by
+  intro C hC
+  contrapose!
+  exact h C hC
+
+lemma nonempty_iInter (hp : IsCompactSystem S) {C : ℕ → Set α} (hC : ∀ i, C i ∈ S)
+    (h_nonempty : ∀ n, (dissipate C n).Nonempty) :
+    (⋂ i, C i).Nonempty := by
+  revert h_nonempty
+  contrapose!
+  exact hp C hC
+
+theorem iff_nonempty_iInter (S : Set (Set α)) :
+    IsCompactSystem S ↔
+      ∀ C : ℕ → Set α, (∀ i, C i ∈ S) → (∀ n, (dissipate C n).Nonempty) → (⋂ i, C i).Nonempty :=
+  ⟨nonempty_iInter, of_nonempty_iInter⟩
+
+@[simp]
+lemma of_IsEmpty [IsEmpty α] (S : Set (Set α)) : IsCompactSystem S :=
+  fun s _ _ ↦ ⟨0, Set.eq_empty_of_isEmpty (dissipate s 0)⟩
+
+/-- Any subset of a compact system is a compact system. -/
+theorem mono {C D : Set (Set α)} (hD : IsCompactSystem D) (hCD : ∀ s, s ∈ C → s ∈ D) :
+  IsCompactSystem C := fun s hC hs ↦ hD s (fun i ↦ hCD (s i) (hC i)) hs
+
+/-- Inserting `∅` into a compact system gives a compact system. -/
+lemma insert_empty (h : IsCompactSystem S) : IsCompactSystem (insert ∅ S) := by
+  intro s h' hd
+  by_cases g : ∃ n, s n = ∅
+  · use g.choose
+    rw [← subset_empty_iff] at hd ⊢
+    exact (dissipate_subset le_rfl).trans g.choose_spec.le
+  · push_neg at g
+    refine h s (fun i ↦ ?_) hd
+    specialize g i
+    specialize h' i
+    rw [Set.nonempty_iff_ne_empty] at g
+    simpa [g] using h'
+
+/-- Inserting `univ` into a compact system gives a compact system. -/
+lemma insert_univ (h : IsCompactSystem S) : IsCompactSystem (insert univ S) := by
+  rcases isEmpty_or_nonempty α with hα | _
+  · simp
+  rw [IsCompactSystem.iff_nonempty_iInter] at h ⊢
+  intro s h' hd
+  by_cases h₀ : ∀ n, s n ∉ S
+  · simp only [mem_insert_iff, h₀, or_false] at h'
+    simp [h']
+  push_neg at h₀
+  classical
+  let n := Nat.find h₀
+  let s' := fun i ↦ if s i ∈ S then s i else s n
+  have h₁ : ∀ i, s' i ∈ S := by simp [s']; grind
+  have h₂ : ⋂ i, s i = ⋂ i, s' i := by ext; simp; grind
+  apply h₂ ▸ h s' h₁
+  by_contra! h_exists_empty
+  obtain ⟨j, hj⟩ := h_exists_empty
+  have h₃ (v : ℕ) (hv : n ≤ v) : dissipate s v = dissipate s' v:= by ext; simp; grind
+  have h₇ : dissipate s' (max j n) = ∅ := by
+    rw [← subset_empty_iff] at hj ⊢
+    exact (antitone_dissipate (Nat.le_max_left j n)).trans hj
+  specialize h₃ (max j n) (Nat.le_max_right j n)
+  specialize hd (max j n)
+  simp [h₃, h₇] at hd
+
+end IsCompactSystem
+
+/-- In this equivalent formulation for a compact system,
+note that we use `⋂ k < n, C k` rather than `⋂ k ≤ n, C k`. -/
+lemma isCompactSystem_iff_nonempty_iInter_of_lt (S : Set (Set α)) :
+    IsCompactSystem S ↔
+      ∀ C : ℕ → Set α, (∀ i, C i ∈ S) → (∀ n, (⋂ k < n, C k).Nonempty) → (⋂ i, C i).Nonempty := by
+  simp_rw [IsCompactSystem.iff_nonempty_iInter]
+  refine ⟨fun h C hi h'↦ h C hi (fun n ↦ dissipate_eq_iInter_lt ▸ (h' (n + 1))),
+    fun h C hi h' ↦ h C hi ?_⟩
+  simp_rw [Set.nonempty_iff_ne_empty] at h' ⊢
+  refine fun n g ↦ h' n ?_
+  simp_rw [← subset_empty_iff, dissipate] at g ⊢
+  exact le_trans (fun x ↦ by simp; grind) g
+
+/-- A set system is a compact system iff adding `∅` gives a compact system. -/
+lemma isCompactSystem_insert_empty_iff :
+    IsCompactSystem (insert ∅ S) ↔ IsCompactSystem S :=
+  ⟨fun h ↦ h.mono (fun _ hs ↦ Set.mem_insert_of_mem ∅ hs), fun h ↦ h.insert_empty⟩
+
+/-- A set system is a compact system iff adding `univ` gives a compact system. -/
+lemma isCompactSystem_insert_univ_iff : IsCompactSystem (insert univ S) ↔ IsCompactSystem S :=
+  ⟨fun h ↦ h.mono (fun _ hs ↦ Set.mem_insert_of_mem univ hs), fun h ↦ h.insert_univ⟩
+
+theorem isCompactSystem_iff_directed (hpi : IsPiSystem S) :
+    IsCompactSystem S ↔
+    ∀ (C : ℕ → Set α), (Directed (fun x1 x2 ↦ x1 ⊇ x2) C) → (∀ i, C i ∈ S) → ⋂ i, C i = ∅ →
+      ∃ n, C n = ∅ := by
+  rw [← isCompactSystem_insert_empty_iff]
+  refine ⟨fun h ↦ fun C hdi hi ↦ ?_, fun h C h1 h2 ↦ ?_⟩
+  · rw [exists_dissipate_eq_empty_iff_of_directed C hdi]
+    exact h C (by simp [hi])
+  · have hpi' : IsPiSystem (insert ∅ S) := hpi.insert_empty
+    rw [← biInter_le_eq_iInter] at h2
+    obtain h' := h (dissipate C) directed_dissipate
+    have h₀ (h₀ : ∀ n, dissipate C n ∈ S ∨ dissipate C n = ∅) (h₁ : ⋂ n, dissipate C n = ∅) :
+        ∃ n, dissipate C n = ∅ := by
+      by_cases! f : ∀ n, dissipate C n ∈ S
+      · apply h' f h₁
+      · obtain ⟨n, hn⟩ := f
+        exact ⟨n, by simpa [hn] using h₀ n⟩
+    obtain h'' := IsPiSystem.dissipate_mem hpi' h1
+    have h₁ : ∀ n, dissipate C n ∈ S ∨ dissipate C n = ∅ := by
+      intro n
+      by_cases g : (dissipate C n).Nonempty
+      · simpa [or_comm] using h'' n g
+      · exact .inr (Set.not_nonempty_iff_eq_empty.mp g)
+    apply h₀ h₁ h2
+
+theorem isCompactSystem_iff_directed' (hpi : IsPiSystem S) :
+    IsCompactSystem S ↔
+    ∀ (C : ℕ → Set α), (Directed (fun x1 x2 ↦ x1 ⊇ x2) C) → (∀ i, C i ∈ S) → (∀ 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
+
+/-- The set of compact and closed sets is a compact system. -/
+theorem isCompactSystem_isCompact_isClosed (α : Type*) [TopologicalSpace α] :
+    IsCompactSystem {s : Set α | IsCompact s ∧ IsClosed s} := by
+  refine IsCompactSystem.of_nonempty_iInter fun C hC_cc h_nonempty ↦ ?_
+  rw [← Set.iInter_dissipate]
+  refine IsCompact.nonempty_iInter_of_sequence_nonempty_isCompact_isClosed (Set.dissipate C)
+    (fun n ↦ ?_) h_nonempty ?_ (fun n ↦ ?_)
+  · exact Set.antitone_dissipate (by lia)
+  · simpa using (hC_cc 0).1
+  · induction n with
+    | zero => simp only [Set.dissipate_zero_nat]; exact (hC_cc 0).2
+    | succ n hn =>
+      rw [Set.dissipate_succ]
+      exact hn.inter (hC_cc (n + 1)).2
+
+/-- In a `T2Space` the set of compact sets is a compact system. -/
+theorem isCompactSystem_isCompact (α : Type*) [TopologicalSpace α] [T2Space α] :
+    IsCompactSystem {s : Set α | IsCompact s} := by
+  convert isCompactSystem_isCompact_isClosed α with s
+  exact ⟨fun hs ↦ ⟨hs, hs.isClosed⟩, fun hs ↦ hs.1⟩
+
+/-- The set of sets which are either compact and closed, or `univ`, is a compact system. -/
+theorem isCompactSystem_insert_univ_isCompact_isClosed (α : Type*) [TopologicalSpace α] :
+    IsCompactSystem (insert univ {s : Set α | IsCompact s ∧ IsClosed s}) :=
+  (isCompactSystem_isCompact_isClosed α).insert_univ
+
+end IsCompactIsClosed