From adf405032e36b9749d607a61c6a237a3ab9e06c5 Mon Sep 17 00:00:00 2001 From: pfaffelh Date: Wed, 14 Jan 2026 22:13:29 +0100 Subject: [PATCH 01/20] run mk_all --- Mathlib.lean | 1 + Mathlib/Data/Set/Dissipate.lean | 144 ++++++++++++++++++++++++++++++++ 2 files changed, 145 insertions(+) create mode 100644 Mathlib/Data/Set/Dissipate.lean diff --git a/Mathlib.lean b/Mathlib.lean index eb8d20cf89f142..126e2b9490901b 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -3968,6 +3968,7 @@ public import Mathlib.Data.Set.Constructions public import Mathlib.Data.Set.Countable public import Mathlib.Data.Set.Defs public import Mathlib.Data.Set.Disjoint +public import Mathlib.Data.Set.Dissipate public import Mathlib.Data.Set.Enumerate public import Mathlib.Data.Set.Equitable public import Mathlib.Data.Set.Finite.Basic diff --git a/Mathlib/Data/Set/Dissipate.lean b/Mathlib/Data/Set/Dissipate.lean new file mode 100644 index 00000000000000..dab5d439281991 --- /dev/null +++ b/Mathlib/Data/Set/Dissipate.lean @@ -0,0 +1,144 @@ +/- +Copyright (c) 2025 Peter Pfaffelhuber. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Peter Pfaffelhuber +-/ +module + +public import Mathlib.Data.Set.Accumulate +public 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. + +-/ + +@[expose] public section + +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 + +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, dissipate] + +@[simp] +theorem dissipate_eq_accumulate_compl [LE α] {s : α → Set β} {x : α} : + (Set.accumulate (fun y ↦ (s y)ᶜ) x)ᶜ = dissipate s x := by + simp [accumulate_def, dissipate_def] + +@[simp] +theorem accumulate_eq_dissipate_compl [LE α] {s : α → Set β} {x : α} : + (Set.dissipate (fun y ↦ (s y)ᶜ) x)ᶜ = accumulate s x := by + simp [accumulate_def, dissipate_def] + +@[simp] +theorem mem_dissipate [LE α] {x : α} {z : β} : z ∈ dissipate s x ↔ ∀ y ≤ x, z ∈ s y := by + simp [dissipate_def] + +theorem dissipate_subset [LE α] {x y : α} (hy : y ≤ x) : dissipate s x ⊆ s y := + biInter_subset_of_mem hy + +theorem iInter_subset_dissipate [LE α] (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), dissipate s y = dissipate s x := by + apply Subset.antisymm + · apply iInter_mono fun z y hy ↦ ?_ + simp only [mem_iInter, mem_dissipate] at * + exact fun h ↦ hy h z (le_refl z) + · simp only [subset_iInter_iff] + exact fun i j ↦ dissipate_subset_dissipate j + +@[simp] +theorem iInter_dissipate [Preorder α] : ⋂ x, dissipate s x = ⋂ x, s x := by + apply Subset.antisymm <;> simp_rw [subset_def, dissipate_def, mem_iInter] + · exact fun z h x' ↦ h x' x' (le_refl x') + · exact fun z h x' y hy ↦ h y + +@[simp] +lemma dissipate_bot [PartialOrder α] [OrderBot α] (s : α → Set β) : dissipate s ⊥ = s ⊥ := by + simp [dissipate_def] + +open Nat + +@[simp] +theorem dissipate_succ (s : ℕ → Set α) (n : ℕ) : + dissipate s (n + 1) = (dissipate s n) ∩ s (n + 1) + := by + ext x + simp_all only [dissipate_def, mem_iInter, mem_inter_iff] + grind + +@[simp] +lemma dissipate_zero (s : ℕ → Set β) : dissipate s 0 = s 0 := by + simp [dissipate_def] + +/-- For a directed set of sets `s : ℕ → Set α` (i.e. `∀ i j, ∃ k, s k ⊆ s i ∩ s j`) 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 + simp_rw [dissipate_succ] + obtain ⟨k, hk⟩ := hd m (n+1) + simp only at hk + use k + simp only [subset_inter_iff] + exact ⟨le_trans hk.1 hm, hk.2⟩ + +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, dissipate C n = ∅) ↔ (∃ n, C 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) + · exact subset_eq_empty (dissipate_subset (Nat.le_refl n)) hn + +/-- For a ∩-stable set of sets `p` on `α` and a sequence of sets `s` with this attribute, +`dissipate s n` belongs to `p`. -/ +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_succ] at * + apply hp (dissipate s n) (hn (Nonempty.left h')) (s (n+1)) (h (n+1)) h' + +end Set From 3fffde0d8cbd644c6ae8af7fa6c90b52e0deace7 Mon Sep 17 00:00:00 2001 From: pfaffelh Date: Mon, 2 Mar 2026 23:50:56 +0100 Subject: [PATCH 02/20] like pfaffelh_compactSystem but in the module system --- Mathlib/Data/Set/Dissipate.lean | 47 +++ .../Topology/Compactness/CompactSystem.lean | 286 ++++++++++++++++++ 2 files changed, 333 insertions(+) create mode 100644 Mathlib/Topology/Compactness/CompactSystem.lean diff --git a/Mathlib/Data/Set/Dissipate.lean b/Mathlib/Data/Set/Dissipate.lean index ee403dacb2b95f..8757e7fe156b31 100644 --- a/Mathlib/Data/Set/Dissipate.lean +++ b/Mathlib/Data/Set/Dissipate.lean @@ -7,6 +7,7 @@ Authors: Peter Pfaffelhuber module public import Mathlib.Data.Set.Accumulate +public import Mathlib.MeasureTheory.PiSystem /-! # Dissipate @@ -28,6 +29,9 @@ def dissipate [LE α] (s : α → Set β) (x : α) : Set β := 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, dissipate] + @[simp] theorem mem_dissipate [LE α] {x : α} {z : β} : z ∈ dissipate s x ↔ ∀ y ≤ x, z ∈ s y := by simp [dissipate_def] @@ -80,4 +84,47 @@ 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 + simp_rw [dissipate_succ] + obtain ⟨k, hk⟩ := hd m (n+1) + simp only at hk + use k + simp only [subset_inter_iff] + exact ⟨le_trans hk.1 hm, hk.2⟩ + +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, ?_⟩ , ?_⟩ + · exact subset_eq_empty (dissipate_subset (Nat.le_refl n)) hn + · 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, +`dissipate s n` belongs to `p`. -/ +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, Nat.le_zero_eq, iInter_iInter_eq_left] + exact h 0 + | succ n hn => + rw [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/Topology/Compactness/CompactSystem.lean b/Mathlib/Topology/Compactness/CompactSystem.lean new file mode 100644 index 00000000000000..9c35597af62d23 --- /dev/null +++ b/Mathlib/Topology/Compactness/CompactSystem.lean @@ -0,0 +1,286 @@ +/- +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.Data.Set.Dissipate +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 + +* `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`. +-/ + +@[expose] public section + +open Set Finset Nat + +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] + +/-- 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] + apply 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⟩ + rw [h] + apply (of_isCompact_isClosed) + +end IsCompactIsClosed + +end IsCompactSystem From aea7a8538bb0452aa77c74bc47bb449223503888 Mon Sep 17 00:00:00 2001 From: pfaffelh Date: Tue, 3 Mar 2026 00:13:08 +0100 Subject: [PATCH 03/20] update one lemma --- .../Topology/Compactness/CompactSystem.lean | 22 ++++++++----------- 1 file changed, 9 insertions(+), 13 deletions(-) diff --git a/Mathlib/Topology/Compactness/CompactSystem.lean b/Mathlib/Topology/Compactness/CompactSystem.lean index 9c35597af62d23..d4dd9483891cba 100644 --- a/Mathlib/Topology/Compactness/CompactSystem.lean +++ b/Mathlib/Topology/Compactness/CompactSystem.lean @@ -72,19 +72,15 @@ 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 + refine ⟨fun h C hi h'↦ h C hi (fun n ↦ dissipate_eq ▸ (h' (n + 1))), fun h C hi h' ↦ h C hi ?_⟩ + simp_rw [Set.nonempty_iff_ne_empty] at h' ⊢ + intro n 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) : From 00181ac889421299ce3026323f2f0f19b20050f0 Mon Sep 17 00:00:00 2001 From: pfaffelh Date: Tue, 3 Mar 2026 00:13:59 +0100 Subject: [PATCH 04/20] update one lemma2 --- Mathlib.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Mathlib.lean b/Mathlib.lean index 3d0097ea74ddf6..74419b89532705 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -7262,6 +7262,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 From 47ab101dcf3283fd3e33659ac576cd0e65e41714 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Tue, 3 Mar 2026 10:19:20 +0100 Subject: [PATCH 05/20] golf; revert an import --- Mathlib/Data/Set/Dissipate.lean | 14 - Mathlib/MeasureTheory/PiSystem.lean | 14 + .../Topology/Compactness/CompactSystem.lean | 263 +++++++----------- 3 files changed, 116 insertions(+), 175 deletions(-) diff --git a/Mathlib/Data/Set/Dissipate.lean b/Mathlib/Data/Set/Dissipate.lean index 8757e7fe156b31..c42b516a38ebf4 100644 --- a/Mathlib/Data/Set/Dissipate.lean +++ b/Mathlib/Data/Set/Dissipate.lean @@ -7,7 +7,6 @@ Authors: Peter Pfaffelhuber module public import Mathlib.Data.Set.Accumulate -public import Mathlib.MeasureTheory.PiSystem /-! # Dissipate @@ -114,17 +113,4 @@ lemma exists_dissipate_eq_empty_iff_of_directed (C : ℕ → Set α) 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, -`dissipate s n` belongs to `p`. -/ -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, Nat.le_zero_eq, iInter_iInter_eq_left] - exact h 0 - | succ n hn => - rw [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/MeasureTheory/PiSystem.lean b/Mathlib/MeasureTheory/PiSystem.lean index 768a1832c37b38..1ec23e26462add 100644 --- a/Mathlib/MeasureTheory/PiSystem.lean +++ b/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 @@ -695,3 +696,16 @@ theorem induction_on_inter {m : MeasurableSpace α} {C : ∀ s : Set α, Measura | @iUnion f hfd hf ihf => exact iUnion f hfd (eq ▸ hf) ihf end MeasurableSpace + +/-- For a ∩-stable set of sets `p` on `α` and a sequence of sets `s` with this attribute, +`dissipate s n` belongs to `p`. -/ +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, Nat.le_zero_eq, iInter_iInter_eq_left] + exact h 0 + | succ n hn => + rw [dissipate_succ] at * + apply hp (dissipate s n) (hn (Nonempty.left h')) (s (n+1)) (h (n+1)) h' diff --git a/Mathlib/Topology/Compactness/CompactSystem.lean b/Mathlib/Topology/Compactness/CompactSystem.lean index d4dd9483891cba..bdc30ac9d50dcc 100644 --- a/Mathlib/Topology/Compactness/CompactSystem.lean +++ b/Mathlib/Topology/Compactness/CompactSystem.lean @@ -6,6 +6,7 @@ Authors: Rémy Degenne, Peter Pfaffelhuber module public import Mathlib.Data.Set.Dissipate +public import Mathlib.MeasureTheory.PiSystem public import Mathlib.Topology.Separation.Hausdorff /-! @@ -58,19 +59,38 @@ lemma dissipate_eq_empty (hp : IsCompactSystem p) (hC : ∀ i, p (C i)) dissipate C (hp.finite_of_empty hC hC_empty) = ∅ := by apply Nat.find_spec (hp C hC hC_empty) +lemma of_nonempty_iInter + (h : ∀ C : ℕ → Set α, (∀ i, p (C i)) → (∀ n, (dissipate C n).Nonempty) → (⋂ i, C i).Nonempty) : + IsCompactSystem p := by + intro C hC + contrapose! + exact h C hC + +lemma nonempty_iInter (hp : IsCompactSystem p) {C : ℕ → Set α} (hC : ∀ i, p (C i)) + (h_nonempty : ∀ n, (dissipate C n).Nonempty) : + (⋂ i, C i).Nonempty := by + revert h_nonempty + contrapose! + exact hp C hC + 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 + (dissipate C n).Nonempty) → (⋂ i, C i).Nonempty) := + ⟨nonempty_iInter, of_nonempty_iInter⟩ + +@[simp] +lemma of_IsEmpty [IsEmpty α] (p : Set α → Prop) : IsCompactSystem p := + 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 α) → 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 /-- 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 +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'↦ h C hi (fun n ↦ dissipate_eq ▸ (h' (n + 1))), fun h C hi h' ↦ h C hi ?_⟩ simp_rw [Set.nonempty_iff_ne_empty] at h' ⊢ @@ -82,138 +102,82 @@ lemma iff_nonempty_iInter_of_lt (p : Set α → Prop) : IsCompactSystem p ↔ 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))⟩ +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.inr a).symm)⟩ 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 + exact (dissipate_subset le_rfl).trans 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)⟩ + refine h s (fun i ↦ ?_) hd + specialize g i + specialize h' i + rw [Set.nonempty_iff_ne_empty] at g + simpa [g] using h' /-- 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 +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) : + rcases isEmpty_or_nonempty α with hα | _ + · simp + rw [iff_nonempty_iInter] at h ⊢ + intro s h' hd + by_cases h₀ : ∀ n, ¬ p (s n) + · simp only [h₀, false_or] at h' + simp [h'] + push_neg at h₀ + classical + 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 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 + +theorem iff_directed (hpi : IsPiSystem {x |p x}) : IsCompactSystem p ↔ - ∀ (C : ℕ → Set α), ∀ (_ : Directed (fun (x1 x2 : Set α) => x1 ⊇ x2) C), (∀ i, p (C i)) → - ⋂ i, C i = ∅ → ∃ (n : ℕ), C n = ∅ := by + ∀ (C : ℕ → Set α), (Directed (fun x1 x2 ↦ 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 + exact h C (by simp [hi]) + · have hpi' : IsPiSystem {s | p s ∨ s = ∅} := by + convert IsPiSystem.insert_empty hpi using 1 + ext + simp + grind 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) + have h₀ (h₀ : ∀ n, p (dissipate C n) ∨ dissipate C n = ∅) (h₁ : ⋂ n, dissipate C n = ∅) : + ∃ n, dissipate C n = ∅ := by + 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 ⟨n, hn⟩ := f + exact ⟨n, by simpa [hn] using h₀ n⟩ obtain h'' := IsPiSystem.dissipate_mem hpi' h1 - have h₁ : ∀ (n : ℕ), p (dissipate C n) ∨ dissipate C n = ∅ := by + 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 + · exact .inr (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 + ∀ (C : ℕ → Set α), (Directed (fun x1 x2 ↦ 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 @@ -226,41 +190,27 @@ 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] + intro C hC_cc hC_inter + by_contra! h_nonempty + refine absurd hC_inter ?_ + rw [← ne_eq, ← Set.nonempty_iff_ne_empty, ← Set.iInter_dissipate] + refine IsCompact.nonempty_iInter_of_sequence_nonempty_isCompact_isClosed (Set.dissipate C) + (fun n ↦ ?_) (fun n ↦ ?_) ?_ (fun n ↦ ?_) + · exact Set.antitone_dissipate (by lia) + · exact h_nonempty _ + · simp only [Set.dissipate_zero_nat] + exact (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 of_isCompact [T2Space α] : + IsCompactSystem (fun s : Set α ↦ IsCompact s) := by + convert of_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 of_isCompact_isClosed_or_univ : @@ -268,15 +218,6 @@ theorem of_isCompact_isClosed_or_univ : rw [← iff_isCompactSystem_of_or_univ] apply 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⟩ - rw [h] - apply (of_isCompact_isClosed) - end IsCompactIsClosed end IsCompactSystem From 4ee793da46bf002a785798ec1689e327c898b76f Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Tue, 3 Mar 2026 10:28:58 +0100 Subject: [PATCH 06/20] golf --- Mathlib/Data/Set/Dissipate.lean | 25 +++++++------------ .../Topology/Compactness/CompactSystem.lean | 3 +-- 2 files changed, 10 insertions(+), 18 deletions(-) diff --git a/Mathlib/Data/Set/Dissipate.lean b/Mathlib/Data/Set/Dissipate.lean index c42b516a38ebf4..940a33d8b55831 100644 --- a/Mathlib/Data/Set/Dissipate.lean +++ b/Mathlib/Data/Set/Dissipate.lean @@ -28,7 +28,7 @@ def dissipate [LE α] (s : α → Set β) (x : α) : Set β := 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 +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] @@ -91,26 +91,19 @@ lemma exists_subset_dissipate_of_directed {s : ℕ → Set α} | zero => use 0; simp [dissipate_def] | succ n hn => obtain ⟨m, hm⟩ := hn - simp_rw [dissipate_succ] obtain ⟨k, hk⟩ := hd m (n+1) - simp only at hk - use k - simp only [subset_inter_iff] - exact ⟨le_trans hk.1 hm, hk.2⟩ + exact ⟨k, by simp; grind⟩ -lemma directed_dissipate {s : ℕ → Set α} : - Directed (fun (x y : Set α) => y ⊆ x) (dissipate s) := +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 : Set α) => y ⊆ x) C) : + (hd : Directed (fun x y ↦ y ⊆ x) C) : (∃ n, C n = ∅) ↔ (∃ n, dissipate C n = ∅) := by - refine ⟨fun ⟨n, hn⟩ ↦ ⟨n, ?_⟩ , ?_⟩ - · exact subset_eq_empty (dissipate_subset (Nat.le_refl n)) hn - · 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) + 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 diff --git a/Mathlib/Topology/Compactness/CompactSystem.lean b/Mathlib/Topology/Compactness/CompactSystem.lean index bdc30ac9d50dcc..26a466cf0077ee 100644 --- a/Mathlib/Topology/Compactness/CompactSystem.lean +++ b/Mathlib/Topology/Compactness/CompactSystem.lean @@ -5,7 +5,6 @@ Authors: Rémy Degenne, Peter Pfaffelhuber -/ module -public import Mathlib.Data.Set.Dissipate public import Mathlib.MeasureTheory.PiSystem public import Mathlib.Topology.Separation.Hausdorff @@ -21,7 +20,7 @@ This file defines compact systems of sets. ## Main results -* `IsCompactSystemiff_isCompactSystem_of_or_univ`: A set system is a compact +* `IsCompactSystem.iff_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 From e778b5e633afb102b57ffc549cbab13b27c44de9 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Tue, 3 Mar 2026 10:32:25 +0100 Subject: [PATCH 07/20] move and golf --- Mathlib/MeasureTheory/PiSystem.lean | 24 +++++++++++------------- 1 file changed, 11 insertions(+), 13 deletions(-) diff --git a/Mathlib/MeasureTheory/PiSystem.lean b/Mathlib/MeasureTheory/PiSystem.lean index 1ec23e26462add..68ebda266c65d1 100644 --- a/Mathlib/MeasureTheory/PiSystem.lean +++ b/Mathlib/MeasureTheory/PiSystem.lean @@ -108,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 @@ -696,16 +707,3 @@ theorem induction_on_inter {m : MeasurableSpace α} {C : ∀ s : Set α, Measura | @iUnion f hfd hf ihf => exact iUnion f hfd (eq ▸ hf) ihf end MeasurableSpace - -/-- For a ∩-stable set of sets `p` on `α` and a sequence of sets `s` with this attribute, -`dissipate s n` belongs to `p`. -/ -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, Nat.le_zero_eq, iInter_iInter_eq_left] - exact h 0 - | succ n hn => - rw [dissipate_succ] at * - apply hp (dissipate s n) (hn (Nonempty.left h')) (s (n+1)) (h (n+1)) h' From c4c2236bdee8828d129a0185f8fb9c0d1acca744 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Tue, 3 Mar 2026 10:37:07 +0100 Subject: [PATCH 08/20] golf --- Mathlib/Topology/Compactness/CompactSystem.lean | 11 ++++------- 1 file changed, 4 insertions(+), 7 deletions(-) diff --git a/Mathlib/Topology/Compactness/CompactSystem.lean b/Mathlib/Topology/Compactness/CompactSystem.lean index 26a466cf0077ee..42f3d195b8087d 100644 --- a/Mathlib/Topology/Compactness/CompactSystem.lean +++ b/Mathlib/Topology/Compactness/CompactSystem.lean @@ -91,15 +91,12 @@ 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'↦ h C hi (fun n ↦ dissipate_eq ▸ (h' (n + 1))), fun h C hi h' ↦ h C hi ?_⟩ + 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' ⊢ - intro n g - apply h' n + refine fun n g ↦ 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 + exact le_trans (fun x ↦ by simp; grind) g /-- A set system is a compact system iff adding `∅` gives a compact system. -/ lemma iff_isCompactSystem_of_or_empty : From a2feb8f863deabc27eca92bc0cf569f135b8258b Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Tue, 3 Mar 2026 10:46:07 +0100 Subject: [PATCH 09/20] follow in-person review: switch to sets of sets --- .../Topology/Compactness/CompactSystem.lean | 82 +++++++++---------- 1 file changed, 39 insertions(+), 43 deletions(-) diff --git a/Mathlib/Topology/Compactness/CompactSystem.lean b/Mathlib/Topology/Compactness/CompactSystem.lean index 42f3d195b8087d..449b48fde4da9d 100644 --- a/Mathlib/Topology/Compactness/CompactSystem.lean +++ b/Mathlib/Topology/Compactness/CompactSystem.lean @@ -9,7 +9,7 @@ public import Mathlib.MeasureTheory.PiSystem public import Mathlib.Topology.Separation.Hausdorff /-! -# Compact systems. +# Compact systems This file defines compact systems of sets. @@ -31,14 +31,14 @@ system iff inserting `univ` gives a compact system. open Set Finset Nat -variable {α : Type*} {p : Set α → Prop} {C : ℕ → Set α} +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 (p : Set α → Prop) : Prop := - ∀ C : ℕ → Set α, (∀ i, p (C i)) → ⋂ i, C i = ∅ → ∃ (n : ℕ), dissipate C n = ∅ +def IsCompactSystem (S : Set (Set α)) : Prop := + ∀ C : ℕ → Set α, (∀ i, C i ∈ S) → ⋂ i, C i = ∅ → ∃ (n : ℕ), dissipate C n = ∅ end definition @@ -48,48 +48,48 @@ 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)) +def finite_of_empty (hp : IsCompactSystem S) (hC : ∀ i, C i ∈ S) (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)) +lemma dissipate_eq_empty (hp : IsCompactSystem S) (hC : ∀ i, C i ∈ S) (hC_empty : ⋂ i, C i = ∅) : dissipate C (hp.finite_of_empty hC hC_empty) = ∅ := by apply Nat.find_spec (hp C hC hC_empty) lemma of_nonempty_iInter - (h : ∀ C : ℕ → Set α, (∀ i, p (C i)) → (∀ n, (dissipate C n).Nonempty) → (⋂ i, C i).Nonempty) : - IsCompactSystem p := by + (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 p) {C : ℕ → Set α} (hC : ∀ i, p (C i)) +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 (p : Set α → Prop) : - IsCompactSystem p ↔ (∀ C : ℕ → Set α, (∀ i, p (C i)) → (∀ (n : ℕ), - (dissipate C n).Nonempty) → (⋂ i, C i).Nonempty) := +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 α] (p : Set α → Prop) : IsCompactSystem p := +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 α) → Prop} (hD : IsCompactSystem D) (hCD : ∀ s, C s → D s) : +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 /-- 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 +lemma 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 [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 ?_⟩ @@ -100,8 +100,8 @@ lemma iff_nonempty_iInter_of_lt (p : Set α → Prop) : /-- 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.inr a).symm)⟩ + IsCompactSystem S ↔ IsCompactSystem (insert ∅ S) := by + refine ⟨fun h s h' hd ↦ ?_, fun h ↦ mono h (fun s hs ↦ Set.mem_insert_of_mem ∅ hs)⟩ by_cases g : ∃ n, s n = ∅ · use g.choose rw [← subset_empty_iff] at hd ⊢ @@ -115,20 +115,20 @@ lemma iff_isCompactSystem_of_or_empty : /-- 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))⟩ + IsCompactSystem S ↔ IsCompactSystem (insert univ S) := by + refine ⟨fun h ↦ ?_, fun h ↦ mono h (fun s hs ↦ Set.mem_insert_of_mem univ hs)⟩ rcases isEmpty_or_nonempty α with hα | _ · simp rw [iff_nonempty_iInter] at h ⊢ intro s h' hd - by_cases h₀ : ∀ n, ¬ p (s n) - · simp only [h₀, false_or] at h' + 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 p (s i) then s i else s n - have h₁ : ∀ i, p (s' i) := by simp [s']; grind + 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 @@ -141,38 +141,34 @@ lemma iff_isCompactSystem_of_or_univ : specialize hd (max j n) simp [h₃, h₇] at hd -theorem iff_directed (hpi : IsPiSystem {x |p x}) : - IsCompactSystem p ↔ - ∀ (C : ℕ → Set α), (Directed (fun x1 x2 ↦ x1 ⊇ x2) C) → (∀ i, p (C i)) → ⋂ i, C i = ∅ → +theorem 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 [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] exact h C (by simp [hi]) - · have hpi' : IsPiSystem {s | p s ∨ s = ∅} := by - convert IsPiSystem.insert_empty hpi using 1 - ext - simp - grind + · 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, p (dissipate C n) ∨ dissipate C n = ∅) (h₁ : ⋂ n, dissipate C n = ∅) : + 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, p (dissipate C n) + 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, p (dissipate C n) ∨ dissipate C n = ∅ := by + have h₁ : ∀ n, dissipate C n ∈ S ∨ dissipate C n = ∅ := by intro n by_cases g : (dissipate C n).Nonempty - · exact h'' n g + · simpa [or_comm] using h'' n g · exact .inr (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 ↦ x1 ⊇ x2) C) → (∀ i, p (C i)) → (∀ n, (C n).Nonempty) → +theorem 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 @@ -185,7 +181,7 @@ 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 + IsCompactSystem {s : Set α | IsCompact s ∧ IsClosed s} := by intro C hC_cc hC_inter by_contra! h_nonempty refine absurd hC_inter ?_ @@ -204,13 +200,13 @@ theorem 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 + IsCompactSystem {s : Set α | IsCompact s} := by convert of_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 of_isCompact_isClosed_or_univ : - IsCompactSystem (fun s : Set α ↦ (IsCompact s ∧ IsClosed s) ∨ (s = univ)) := by + IsCompactSystem (insert univ {s : Set α | IsCompact s ∧ IsClosed s}) := by rw [← iff_isCompactSystem_of_or_univ] apply of_isCompact_isClosed From 41caa5ae49a7c0b4ed7f267c4245cd34520f674f Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Tue, 3 Mar 2026 11:04:47 +0100 Subject: [PATCH 10/20] extract lemmas --- .../Topology/Compactness/CompactSystem.lean | 112 ++++++++---------- 1 file changed, 48 insertions(+), 64 deletions(-) diff --git a/Mathlib/Topology/Compactness/CompactSystem.lean b/Mathlib/Topology/Compactness/CompactSystem.lean index 449b48fde4da9d..1fea1859b81671 100644 --- a/Mathlib/Topology/Compactness/CompactSystem.lean +++ b/Mathlib/Topology/Compactness/CompactSystem.lean @@ -20,11 +20,10 @@ This file defines compact systems of sets. ## Main results -* `IsCompactSystem.iff_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_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 @@ -44,20 +43,6 @@ 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 S) (hC : ∀ i, C i ∈ S) - (hC_empty : ⋂ i, C i = ∅) : ℕ := - Nat.find (hp C hC hC_empty) - -open Classical in -lemma dissipate_eq_empty (hp : IsCompactSystem S) (hC : ∀ i, C i ∈ S) - (hC_empty : ⋂ i, C i = ∅) : - dissipate C (hp.finite_of_empty hC hC_empty) = ∅ := by - apply Nat.find_spec (hp C hC hC_empty) - lemma of_nonempty_iInter (h : ∀ C : ℕ → Set α, (∀ i, C i ∈ S) → (∀ n, (dissipate C n).Nonempty) → (⋂ i, C i).Nonempty) : IsCompactSystem S := by @@ -85,23 +70,9 @@ lemma of_IsEmpty [IsEmpty α] (S : Set (Set α)) : IsCompactSystem S := 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 -/-- 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 (S : Set (Set α)) : - IsCompactSystem S ↔ - ∀ C : ℕ → Set α, (∀ i, C i ∈ S) → (∀ n, (⋂ k < n, C k).Nonempty) → (⋂ i, C i).Nonempty := by - simp_rw [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 iff_isCompactSystem_of_or_empty : - IsCompactSystem S ↔ IsCompactSystem (insert ∅ S) := by - refine ⟨fun h s h' hd ↦ ?_, fun h ↦ mono h (fun s hs ↦ Set.mem_insert_of_mem ∅ 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 ⊢ @@ -113,13 +84,11 @@ lemma iff_isCompactSystem_of_or_empty : rw [Set.nonempty_iff_ne_empty] at g simpa [g] using h' -/-- A set system is a compact system iff adding `univ` gives a compact system. -/ -lemma iff_isCompactSystem_of_or_univ : - IsCompactSystem S ↔ IsCompactSystem (insert univ S) := by - refine ⟨fun h ↦ ?_, fun h ↦ mono h (fun s hs ↦ Set.mem_insert_of_mem univ hs)⟩ +/-- 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 [iff_nonempty_iInter] at h ⊢ + 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' @@ -141,11 +110,35 @@ lemma iff_isCompactSystem_of_or_univ : specialize hd (max j n) simp [h₃, h₇] at hd -theorem iff_directed (hpi : IsPiSystem S) : +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 [iff_isCompactSystem_of_or_empty] + 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]) @@ -166,32 +159,26 @@ theorem iff_directed (hpi : IsPiSystem S) : · exact .inr (Set.not_nonempty_iff_eq_empty.mp g) apply h₀ h₁ h2 -theorem iff_directed' (hpi : IsPiSystem S) : +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] + 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 : +theorem isCompactSystem_isCompact_isClosed (α : Type*) [TopologicalSpace α] : IsCompactSystem {s : Set α | IsCompact s ∧ IsClosed s} := by - intro C hC_cc hC_inter - by_contra! h_nonempty - refine absurd hC_inter ?_ - rw [← ne_eq, ← Set.nonempty_iff_ne_empty, ← Set.iInter_dissipate] + 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 ↦ ?_) (fun n ↦ ?_) ?_ (fun n ↦ ?_) + (fun n ↦ ?_) h_nonempty ?_ (fun n ↦ ?_) · exact Set.antitone_dissipate (by lia) - · exact h_nonempty _ - · simp only [Set.dissipate_zero_nat] - exact (hC_cc 0).1 + · simpa using (hC_cc 0).1 · induction n with | zero => simp only [Set.dissipate_zero_nat]; exact (hC_cc 0).2 | succ n hn => @@ -199,17 +186,14 @@ theorem of_isCompact_isClosed : exact hn.inter (hC_cc (n + 1)).2 /-- In a `T2Space` the set of compact sets is a compact system. -/ -theorem of_isCompact [T2Space α] : +theorem isCompactSystem_isCompact (α : Type*) [TopologicalSpace α] [T2Space α] : IsCompactSystem {s : Set α | IsCompact s} := by - convert of_isCompact_isClosed α with s + 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 of_isCompact_isClosed_or_univ : - IsCompactSystem (insert univ {s : Set α | IsCompact s ∧ IsClosed s}) := by - rw [← iff_isCompactSystem_of_or_univ] - apply of_isCompact_isClosed +theorem isCompactSystem_insert_univ_isCompact_isClosed (α : Type*) [TopologicalSpace α] : + IsCompactSystem (insert univ {s : Set α | IsCompact s ∧ IsClosed s}) := + (isCompactSystem_isCompact_isClosed α).insert_univ end IsCompactIsClosed - -end IsCompactSystem From 11115229ab78f6cbfaaa6331487dcebc50863913 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=A9my=20Degenne?= Date: Wed, 4 Mar 2026 12:11:29 +0100 Subject: [PATCH 11/20] Apply suggestions from code review Co-authored-by: Etienne Marion <66847262+EtienneC30@users.noreply.github.com> --- Mathlib/Data/Set/Dissipate.lean | 13 ++-- Mathlib/MeasureTheory/PiSystem.lean | 2 +- .../Topology/Compactness/CompactSystem.lean | 63 +++++++------------ 3 files changed, 30 insertions(+), 48 deletions(-) diff --git a/Mathlib/Data/Set/Dissipate.lean b/Mathlib/Data/Set/Dissipate.lean index 940a33d8b55831..70cd2d18ad71c4 100644 --- a/Mathlib/Data/Set/Dissipate.lean +++ b/Mathlib/Data/Set/Dissipate.lean @@ -28,7 +28,7 @@ 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 +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] @@ -84,22 +84,21 @@ theorem dissipate_succ (s : ℕ → Set α) (n : ℕ) : 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`. -/ +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) + 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) := +lemma directed_dissipate {s : ℕ → Set α} : Directed (· ⊇ ·) (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 +lemma exists_dissipate_eq_empty_iff_of_directed {s : ℕ → Set α} (hd : Directed (· ⊇ ·) s) : + (∃ n, s n = ∅) ↔ (∃ n, dissipate s n = ∅) := by refine ⟨fun ⟨n, hn⟩ ↦ ⟨n, subset_eq_empty (dissipate_subset le_rfl) hn⟩ , ?_⟩ contrapose! intro h n diff --git a/Mathlib/MeasureTheory/PiSystem.lean b/Mathlib/MeasureTheory/PiSystem.lean index 68ebda266c65d1..1d87a02b957680 100644 --- a/Mathlib/MeasureTheory/PiSystem.lean +++ b/Mathlib/MeasureTheory/PiSystem.lean @@ -108,7 +108,7 @@ 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, +/-- 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) : diff --git a/Mathlib/Topology/Compactness/CompactSystem.lean b/Mathlib/Topology/Compactness/CompactSystem.lean index 1fea1859b81671..da2b24280f6ad9 100644 --- a/Mathlib/Topology/Compactness/CompactSystem.lean +++ b/Mathlib/Topology/Compactness/CompactSystem.lean @@ -67,8 +67,8 @@ 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 +theorem mono {T : Set (Set α)} (hT : IsCompactSystem T) (hST : S ⊆ T) : + IsCompactSystem S := fun C hC1 hC2 ↦ hT C (fun i ↦ hST (hC1 i)) hC2 /-- Inserting `∅` into a compact system gives a compact system. -/ lemma insert_empty (h : IsCompactSystem S) : IsCompactSystem (insert ∅ S) := by @@ -78,11 +78,7 @@ lemma insert_empty (h : IsCompactSystem S) : IsCompactSystem (insert ∅ S) := b 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' + exact h s (fun i ↦ (mem_of_mem_insert_of_ne (h' i) (g i).ne_empty)) hd /-- Inserting `univ` into a compact system gives a compact system. -/ lemma insert_univ (h : IsCompactSystem S) : IsCompactSystem (insert univ S) := by @@ -91,8 +87,7 @@ lemma insert_univ (h : IsCompactSystem S) : IsCompactSystem (insert univ S) := b 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'] + · simp_all push_neg at h₀ classical let n := Nat.find h₀ @@ -100,9 +95,8 @@ lemma insert_univ (h : IsCompactSystem S) : IsCompactSystem (insert univ S) := b 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 + by_contra! ⟨j, hj⟩ + 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 @@ -128,11 +122,11 @@ lemma isCompactSystem_iff_nonempty_iInter_of_lt (S : Set (Set α)) : /-- 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⟩ + ⟨fun h ↦ h.mono (subset_insert _ _), 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⟩ + ⟨fun h ↦ h.mono (subset_insert _ _), .insert_univ⟩ theorem isCompactSystem_iff_directed (hpi : IsPiSystem S) : IsCompactSystem S ↔ @@ -142,24 +136,18 @@ theorem isCompactSystem_iff_directed (hpi : IsPiSystem S) : 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) : + rw [← biInter_le_eq_iInter] at h2 + suffices (∀ n, dissipate C n ∈ S ∨ dissipate C n = ∅) ∧ (⋂ n, dissipate C n = ∅) by + by_cases! f : ∀ n, dissipate C n ∈ S + · exact h (dissipate C) directed_dissipate f this.2 + · obtain ⟨n, hn⟩ := f + exact ⟨n, by simpa [hn] using this.1 n⟩ + refine ⟨fun n ↦ ?_, h2⟩ + by_cases g : (dissipate C n).Nonempty + · simpa [or_comm] using hpi.insert_empty.dissipate_mem h1 n g + · exact .inr (Set.not_nonempty_iff_eq_empty.mp g) + +theorem isCompactSystem_iff_directed_of_nonempty (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 @@ -174,22 +162,17 @@ section IsCompactIsClosed 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] + rw [← iInter_dissipate] refine IsCompact.nonempty_iInter_of_sequence_nonempty_isCompact_isClosed (Set.dissipate C) - (fun n ↦ ?_) h_nonempty ?_ (fun n ↦ ?_) + (fun n ↦ ?_) h_nonempty ?_ (fun n ↦ isClosed_biInter (fun i _ ↦ (hC_cc i).2)) · 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⟩ + simpa using IsCompact.isClosed /-- The set of sets which are either compact and closed, or `univ`, is a compact system. -/ theorem isCompactSystem_insert_univ_isCompact_isClosed (α : Type*) [TopologicalSpace α] : From c109d6cadadf23e103b3de457898658f69f21eb0 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Wed, 4 Mar 2026 12:14:50 +0100 Subject: [PATCH 12/20] fix --- Mathlib/Data/Set/Dissipate.lean | 2 +- Mathlib/Topology/Compactness/CompactSystem.lean | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/Mathlib/Data/Set/Dissipate.lean b/Mathlib/Data/Set/Dissipate.lean index 70cd2d18ad71c4..b9ddf39f338018 100644 --- a/Mathlib/Data/Set/Dissipate.lean +++ b/Mathlib/Data/Set/Dissipate.lean @@ -86,7 +86,7 @@ theorem dissipate_succ (s : ℕ → Set α) (n : ℕ) : /-- 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 + (hd : Directed (· ⊇ ·) s) (n : ℕ) : ∃ m, s m ⊆ dissipate s n := by induction n with | zero => use 0; simp [dissipate_def] | succ n hn => diff --git a/Mathlib/Topology/Compactness/CompactSystem.lean b/Mathlib/Topology/Compactness/CompactSystem.lean index da2b24280f6ad9..3c726fc9bfbfd7 100644 --- a/Mathlib/Topology/Compactness/CompactSystem.lean +++ b/Mathlib/Topology/Compactness/CompactSystem.lean @@ -112,7 +112,7 @@ 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))), + refine ⟨fun h C hi h'↦ h C hi (fun n ↦ dissipate_eq_biInter_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 ?_ @@ -134,7 +134,7 @@ theorem isCompactSystem_iff_directed (hpi : IsPiSystem S) : ∃ 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] + · rw [exists_dissipate_eq_empty_iff_of_directed hdi] exact h C (by simp [hi]) rw [← biInter_le_eq_iInter] at h2 suffices (∀ n, dissipate C n ∈ S ∨ dissipate C n = ∅) ∧ (⋂ n, dissipate C n = ∅) by From 37cd1521fe2301d3eed2794a1decabe95787c8cc Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Wed, 4 Mar 2026 12:16:41 +0100 Subject: [PATCH 13/20] review --- Mathlib/Topology/Compactness/CompactSystem.lean | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/Mathlib/Topology/Compactness/CompactSystem.lean b/Mathlib/Topology/Compactness/CompactSystem.lean index 3c726fc9bfbfd7..0c4b42cc946566 100644 --- a/Mathlib/Topology/Compactness/CompactSystem.lean +++ b/Mathlib/Topology/Compactness/CompactSystem.lean @@ -122,7 +122,7 @@ lemma isCompactSystem_iff_nonempty_iInter_of_lt (S : Set (Set α)) : /-- 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 (subset_insert _ _), fun h ↦ h.insert_empty⟩ + ⟨fun h ↦ h.mono (subset_insert _ _), .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 := @@ -130,8 +130,7 @@ lemma isCompactSystem_insert_univ_iff : IsCompactSystem (insert univ S) ↔ IsCo 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 + ∀ (C : ℕ → Set α), Directed (· ⊇ ·) 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 hdi] From 9286ee29b5106bb9ee56a33248e145cff55c16f9 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Wed, 4 Mar 2026 12:22:15 +0100 Subject: [PATCH 14/20] names --- Mathlib/Topology/Compactness/CompactSystem.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Mathlib/Topology/Compactness/CompactSystem.lean b/Mathlib/Topology/Compactness/CompactSystem.lean index 0c4b42cc946566..8f8429971d5ec5 100644 --- a/Mathlib/Topology/Compactness/CompactSystem.lean +++ b/Mathlib/Topology/Compactness/CompactSystem.lean @@ -128,7 +128,7 @@ lemma isCompactSystem_insert_empty_iff : lemma isCompactSystem_insert_univ_iff : IsCompactSystem (insert univ S) ↔ IsCompactSystem S := ⟨fun h ↦ h.mono (subset_insert _ _), .insert_univ⟩ -theorem isCompactSystem_iff_directed (hpi : IsPiSystem S) : +theorem isCompactSystem_iff_of_directed (hpi : IsPiSystem S) : IsCompactSystem S ↔ ∀ (C : ℕ → Set α), Directed (· ⊇ ·) C → (∀ i, C i ∈ S) → ⋂ i, C i = ∅ → ∃ n, C n = ∅ := by rw [← isCompactSystem_insert_empty_iff] @@ -146,11 +146,11 @@ theorem isCompactSystem_iff_directed (hpi : IsPiSystem S) : · simpa [or_comm] using hpi.insert_empty.dissipate_mem h1 n g · exact .inr (Set.not_nonempty_iff_eq_empty.mp g) -theorem isCompactSystem_iff_directed_of_nonempty (hpi : IsPiSystem S) : +theorem isCompactSystem_iff_nonempty_iInter_of_directed (hpi : IsPiSystem S) : IsCompactSystem S ↔ - ∀ (C : ℕ → Set α), (Directed (fun x1 x2 ↦ x1 ⊇ x2) C) → (∀ i, C i ∈ S) → (∀ n, (C n).Nonempty) → + ∀ (C : ℕ → Set α), (Directed (· ⊇ ·) C) → (∀ i, C i ∈ S) → (∀ n, (C n).Nonempty) → (⋂ i, C i).Nonempty := by - rw [isCompactSystem_iff_directed hpi] + rw [isCompactSystem_iff_of_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 From 7eee760f8288c465a53adcd2dcf310e25a0c8df1 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Wed, 4 Mar 2026 12:27:00 +0100 Subject: [PATCH 15/20] review --- Mathlib/Data/Set/Accumulate.lean | 3 +++ Mathlib/Topology/Compactness/CompactSystem.lean | 4 ++++ 2 files changed, 7 insertions(+) diff --git a/Mathlib/Data/Set/Accumulate.lean b/Mathlib/Data/Set/Accumulate.lean index 624341f03ef2d2..8bae818150f0d9 100644 --- a/Mathlib/Data/Set/Accumulate.lean +++ b/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] diff --git a/Mathlib/Topology/Compactness/CompactSystem.lean b/Mathlib/Topology/Compactness/CompactSystem.lean index 8f8429971d5ec5..963949292db39f 100644 --- a/Mathlib/Topology/Compactness/CompactSystem.lean +++ b/Mathlib/Topology/Compactness/CompactSystem.lean @@ -128,6 +128,8 @@ lemma isCompactSystem_insert_empty_iff : lemma isCompactSystem_insert_univ_iff : IsCompactSystem (insert univ S) ↔ IsCompactSystem S := ⟨fun h ↦ h.mono (subset_insert _ _), .insert_univ⟩ +/-- To prove that a set of sets is a compact system, it suffices to consider directed families of +sets. -/ theorem isCompactSystem_iff_of_directed (hpi : IsPiSystem S) : IsCompactSystem S ↔ ∀ (C : ℕ → Set α), Directed (· ⊇ ·) C → (∀ i, C i ∈ S) → ⋂ i, C i = ∅ → ∃ n, C n = ∅ := by @@ -146,6 +148,8 @@ theorem isCompactSystem_iff_of_directed (hpi : IsPiSystem S) : · simpa [or_comm] using hpi.insert_empty.dissipate_mem h1 n g · exact .inr (Set.not_nonempty_iff_eq_empty.mp g) +/-- To prove that a set of sets is a compact system, it suffices to consider directed families of +sets. -/ theorem isCompactSystem_iff_nonempty_iInter_of_directed (hpi : IsPiSystem S) : IsCompactSystem S ↔ ∀ (C : ℕ → Set α), (Directed (· ⊇ ·) C) → (∀ i, C i ∈ S) → (∀ n, (C n).Nonempty) → From 0161fd7bcef5a570b56908330dce5497d185087a Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Wed, 4 Mar 2026 12:30:35 +0100 Subject: [PATCH 16/20] add accumulate versions --- Mathlib/Data/Set/Accumulate.lean | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/Mathlib/Data/Set/Accumulate.lean b/Mathlib/Data/Set/Accumulate.lean index 8bae818150f0d9..19d8485ca34991 100644 --- a/Mathlib/Data/Set/Accumulate.lean +++ b/Mathlib/Data/Set/Accumulate.lean @@ -85,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 @@ -93,4 +94,19 @@ 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 + end Set From 82693239f7c8e17287adb48e91ac397afe8a9398 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Wed, 4 Mar 2026 12:31:56 +0100 Subject: [PATCH 17/20] flip iff --- Mathlib/Data/Set/Dissipate.lean | 4 ++-- Mathlib/Topology/Compactness/CompactSystem.lean | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/Mathlib/Data/Set/Dissipate.lean b/Mathlib/Data/Set/Dissipate.lean index b9ddf39f338018..0d2b153f30f149 100644 --- a/Mathlib/Data/Set/Dissipate.lean +++ b/Mathlib/Data/Set/Dissipate.lean @@ -98,8 +98,8 @@ lemma directed_dissipate {s : ℕ → Set α} : Directed (· ⊇ ·) (dissipate antitone_dissipate.directed_ge lemma exists_dissipate_eq_empty_iff_of_directed {s : ℕ → Set α} (hd : Directed (· ⊇ ·) s) : - (∃ n, s n = ∅) ↔ (∃ n, dissipate s n = ∅) := by - refine ⟨fun ⟨n, hn⟩ ↦ ⟨n, subset_eq_empty (dissipate_subset le_rfl) hn⟩ , ?_⟩ + (∃ 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 diff --git a/Mathlib/Topology/Compactness/CompactSystem.lean b/Mathlib/Topology/Compactness/CompactSystem.lean index 963949292db39f..439102fe321e0e 100644 --- a/Mathlib/Topology/Compactness/CompactSystem.lean +++ b/Mathlib/Topology/Compactness/CompactSystem.lean @@ -135,7 +135,7 @@ theorem isCompactSystem_iff_of_directed (hpi : IsPiSystem S) : ∀ (C : ℕ → Set α), Directed (· ⊇ ·) 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 hdi] + · rw [← exists_dissipate_eq_empty_iff_of_directed hdi] exact h C (by simp [hi]) rw [← biInter_le_eq_iInter] at h2 suffices (∀ n, dissipate C n ∈ S ∨ dissipate C n = ∅) ∧ (⋂ n, dissipate C n = ∅) by From a17c917659e171e3e7c352229ed79df4fed3e490 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Wed, 4 Mar 2026 14:27:48 +0100 Subject: [PATCH 18/20] add accumulate lemma --- Mathlib/Data/Set/Accumulate.lean | 9 +++++++++ Mathlib/Data/Set/Dissipate.lean | 2 +- 2 files changed, 10 insertions(+), 1 deletion(-) diff --git a/Mathlib/Data/Set/Accumulate.lean b/Mathlib/Data/Set/Accumulate.lean index 19d8485ca34991..749df4d76567f9 100644 --- a/Mathlib/Data/Set/Accumulate.lean +++ b/Mathlib/Data/Set/Accumulate.lean @@ -109,4 +109,13 @@ lemma exists_subset_accumulate_of_directed {s : ℕ → Set α} 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 diff --git a/Mathlib/Data/Set/Dissipate.lean b/Mathlib/Data/Set/Dissipate.lean index 0d2b153f30f149..f0d281c104912e 100644 --- a/Mathlib/Data/Set/Dissipate.lean +++ b/Mathlib/Data/Set/Dissipate.lean @@ -98,7 +98,7 @@ lemma directed_dissipate {s : ℕ → Set α} : Directed (· ⊇ ·) (dissipate 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 + (∃ 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 From e7ba393095cc681213c0025b595a6036e8a81644 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=A9my=20Degenne?= Date: Wed, 4 Mar 2026 14:29:00 +0100 Subject: [PATCH 19/20] Update Mathlib/Topology/Compactness/CompactSystem.lean Co-authored-by: Etienne Marion <66847262+EtienneC30@users.noreply.github.com> --- Mathlib/Topology/Compactness/CompactSystem.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Mathlib/Topology/Compactness/CompactSystem.lean b/Mathlib/Topology/Compactness/CompactSystem.lean index 439102fe321e0e..46cdbb9783e203 100644 --- a/Mathlib/Topology/Compactness/CompactSystem.lean +++ b/Mathlib/Topology/Compactness/CompactSystem.lean @@ -86,9 +86,8 @@ lemma insert_univ (h : IsCompactSystem S) : IsCompactSystem (insert univ S) := b · simp rw [IsCompactSystem.iff_nonempty_iInter] at h ⊢ intro s h' hd - by_cases h₀ : ∀ n, s n ∉ S + by_cases! h₀ : ∀ n, s n ∉ S · simp_all - push_neg at h₀ classical let n := Nat.find h₀ let s' := fun i ↦ if s i ∈ S then s i else s n From ba8a9881196a2f268f390ded6854a6c310fe317f Mon Sep 17 00:00:00 2001 From: pfaffelh Date: Thu, 5 Mar 2026 00:16:44 +0100 Subject: [PATCH 20/20] init new PR --- Mathlib/Data/Set/Prod.lean | 18 ++++ .../Constructions/Cylinders.lean | 28 +++++- .../Topology/Compactness/CompactSystem.lean | 93 +++++++++++++++++++ 3 files changed, 138 insertions(+), 1 deletion(-) diff --git a/Mathlib/Data/Set/Prod.lean b/Mathlib/Data/Set/Prod.lean index e07a912e01bf27..8f644eb2fce5ec 100644 --- a/Mathlib/Data/Set/Prod.lean +++ b/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] diff --git a/Mathlib/MeasureTheory/Constructions/Cylinders.lean b/Mathlib/MeasureTheory/Constructions/Cylinders.lean index 1b38f5525ec159..7cd3bccb7a13aa 100644 --- a/Mathlib/MeasureTheory/Constructions/Cylinders.lean +++ b/Mathlib/MeasureTheory/Constructions/Cylinders.lean @@ -60,11 +60,37 @@ def squareCylinders (C : ∀ i, Set (Set (α i))) : Set (Set (∀ i, α i)) := {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 diff --git a/Mathlib/Topology/Compactness/CompactSystem.lean b/Mathlib/Topology/Compactness/CompactSystem.lean index 46cdbb9783e203..cdf6a603163b16 100644 --- a/Mathlib/Topology/Compactness/CompactSystem.lean +++ b/Mathlib/Topology/Compactness/CompactSystem.lean @@ -7,6 +7,7 @@ module public import Mathlib.MeasureTheory.PiSystem public import Mathlib.Topology.Separation.Hausdorff +public import Mathlib.MeasureTheory.Constructions.Cylinders /-! # Compact systems @@ -182,3 +183,95 @@ theorem isCompactSystem_insert_univ_isCompact_isClosed (α : Type*) [Topological (isCompactSystem_isCompact_isClosed α).insert_univ end IsCompactIsClosed + +section pi + +namespace Set + +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 [Set.mem_pi, Set.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] + +end Set + +namespace IsCompactSystem + +variable {ι : Type*} {α : ι → Type*} + +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 + +end IsCompactSystem + +end pi + +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 compactClosedSquareCylinders : Set (Set (Π i, α i)) := + MeasureTheory.squareCylinders (fun i ↦ { t : Set (α i) | IsCompact t ∧ IsClosed t }) + +/-- Products of compact and closed sets form a compact system. -/ +theorem IsCompactSystem.compactClosedPi : + IsCompactSystem (univ.pi '' univ.pi (fun i ↦ { t : Set (α i) | IsCompact t ∧ IsClosed t })) := + IsCompactSystem.pi _ (fun _ ↦ isCompactSystem_isCompact_isClosed (α _)) + +theorem IsCompactSystem.compactClosedOrUnivPi : + IsCompactSystem (univ.pi '' univ.pi (fun i ↦ insert univ { t : + Set (α i) | IsCompact t ∧ IsClosed t })) := + IsCompactSystem.pi _ (fun i ↦ isCompactSystem_insert_univ_isCompact_isClosed (α i)) + +/-- Compact and closed square cylinders are a compact system. -/ +theorem isCompactSystem.compactClosedSquareCylinders : + IsCompactSystem (compactClosedSquareCylinders α) := + IsCompactSystem.mono (IsCompactSystem.compactClosedOrUnivPi _) + (MeasureTheory.squareCylinders_subset_of_or_univ _) + +end ClosedCompactSquareCylinders