diff --git a/Mathlib/Data/Set/Prod.lean b/Mathlib/Data/Set/Prod.lean index ded70ca0d94e00..4d082328e57de3 100644 --- a/Mathlib/Data/Set/Prod.lean +++ b/Mathlib/Data/Set/Prod.lean @@ -698,6 +698,21 @@ theorem pi_eq_empty_iff' : s.pi t = ∅ ↔ ∃ i ∈ s, t i = ∅ := by simp [p theorem disjoint_pi : Disjoint (s.pi t₁) (s.pi t₂) ↔ ∃ i ∈ s, Disjoint (t₁ i) (t₂ i) := by simp only [disjoint_iff_inter_eq_empty, ← pi_inter_distrib, pi_eq_empty_iff'] +theorem pi_nonempty_iff' [∀ i, Decidable (i ∈ s)] : + (s.pi t).Nonempty ↔ ∀ i ∈ s, (t i).Nonempty := by + classical + rw [pi_nonempty_iff] + have h := fun i ↦ exists_mem_of_nonempty (α i) + choose y hy using h + refine ⟨fun h i hi ↦ ?_, fun h i ↦ ?_⟩ + · obtain ⟨x, hx⟩ := h i + exact ⟨x, hx hi⟩ + · choose x hx using h + use (if g : i ∈ s then x i g else y i) + intro hi + simp only [hi, ↓reduceDIte] + exact hx i hi + end Nonempty @[simp] @@ -735,6 +750,10 @@ theorem pi_if {p : ι → Prop} [h : DecidablePred p] (s : Set ι) (t₁ t₂ : theorem union_pi : (s₁ ∪ s₂).pi t = s₁.pi t ∩ s₂.pi t := by simp [pi, or_imp, forall_and, setOf_and] +theorem pi_antitone (h : s₁ ⊆ s₂) : s₂.pi t ⊆ s₁.pi t := by + rw [← union_diff_cancel h, union_pi] + exact Set.inter_subset_left + theorem union_pi_inter (ht₁ : ∀ i ∉ s₁, t₁ i = univ) (ht₂ : ∀ i ∉ s₂, t₂ i = univ) : (s₁ ∪ s₂).pi (fun i ↦ t₁ i ∩ t₂ i) = s₁.pi t₁ ∩ s₂.pi t₂ := by @@ -900,6 +919,25 @@ theorem univ_pi_ite (s : Set ι) [DecidablePred (· ∈ s)] (t : ∀ i, Set (α refine forall_congr' fun i => ?_ split_ifs with h <;> simp [h] +lemma pi_image_eq_of_subset {C : (i : ι) → Set (Set (α i))} + (hC : ∀ i, Nonempty (C i)) + {s₁ s₂ : Set ι} [∀ i : ι, Decidable (i ∈ s₁)] + (hst : s₁ ⊆ s₂) : s₁.pi '' s₁.pi C = s₁.pi '' s₂.pi C := by + let C_mem (i : ι) : Set (α i) := ((Set.exists_mem_of_nonempty (C i)).choose : Set (α i)) + have h_mem (i : ι) : C_mem i ∈ C i := by + simp [C_mem] + ext f + refine ⟨fun ⟨x, ⟨hx1, hx2⟩⟩ ↦ ?_, fun ⟨w, ⟨hw1, hw2⟩⟩ ↦ ?_⟩ + · use fun i ↦ if i ∈ s₁ then x i else C_mem i + refine ⟨fun i hi ↦ ?_, ?_⟩ + · by_cases h1 : i ∈ s₁ <;> simp only [h1, ↓reduceIte] + · exact hx1 i h1 + · exact h_mem i + · rw [← hx2] + exact pi_congr rfl (fun i hi ↦ by simp only [hi, ↓reduceIte]) + · have hw3 := pi_antitone hst hw1 + use w + end Pi end Set diff --git a/Mathlib/MeasureTheory/Constructions/Cylinders.lean b/Mathlib/MeasureTheory/Constructions/Cylinders.lean index e2261215ff3185..f327d0530e27ce 100644 --- a/Mathlib/MeasureTheory/Constructions/Cylinders.lean +++ b/Mathlib/MeasureTheory/Constructions/Cylinders.lean @@ -3,9 +3,11 @@ Copyright (c) 2023 Rémy Degenne. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Rémy Degenne, Peter Pfaffelhuber, Yaël Dillies, Kin Yau James Wong -/ +import Mathlib.Data.Finset.Lattice.Basic import Mathlib.MeasureTheory.MeasurableSpace.Constructions -import Mathlib.MeasureTheory.PiSystem +import Mathlib.MeasureTheory.SetSemiring import Mathlib.Topology.Constructions +import Mathlib.MeasureTheory.SetAlgebra /-! # π-systems of cylinders and square cylinders @@ -24,6 +26,8 @@ Given a finite set `s` of indices, a cylinder is the product of a set of `∀ i a product set. * `cylinder s S`: cylinder with base set `S : Set (∀ i : s, α i)` where `s` is a `Finset` +* `squareCylinder s S`: square cylinder with base set `S : (∀ i : s, Set (α i))` where + `s` is a `Finset` * `squareCylinders C` with `C : ∀ i, Set (Set (α i))`: set of all square cylinders such that for all `i` in the finset defining the box, the projection to `α i` belongs to `C i`. The main application of this is with `C i = {s : Set (α i) | MeasurableSet s}`. @@ -48,62 +52,105 @@ variable {ι : Type _} {α : ι → Type _} section squareCylinders -/-- Given a finite set `s` of indices, a square cylinder is the product of a set `S` of -`∀ i : s, α i` and of `univ` on the other indices. The set `S` is a product of sets `t i` such that +/-- Given a finite set `s` of indices, a square cylinder is the product of sets `t i : Set (α i)` +for `i ∈ s` and of `univ` on the other indices. -/ +def squareCylinder (s : Finset ι) (t : ∀ i, Set (α i)) : Set (∀ i, α i) := + (s : Set ι).pi t + +/-- The set `S` is a product of sets `t i` such that for all `i : s`, `t i ∈ C i`. `squareCylinders` is the set of all such squareCylinders. -/ def squareCylinders (C : ∀ i, Set (Set (α i))) : Set (Set (∀ i, α i)) := - {S | ∃ s : Finset ι, ∃ t ∈ univ.pi C, S = (s : Set ι).pi t} + {S | ∃ s : Finset ι, ∃ t ∈ univ.pi C, S = squareCylinder s 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 [squareCylinder, squareCylinders, mem_iUnion, mem_image, mem_univ_pi, exists_prop, + 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_univ_pi, exists_prop, mem_setOf_eq, - eq_comm (a := f)] + simp only [squareCylinder, 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] -theorem isPiSystem_squareCylinders {C : ∀ i, Set (Set (α i))} (hC : ∀ i, IsPiSystem (C i)) - (hC_univ : ∀ i, univ ∈ C i) : - IsPiSystem (squareCylinders C) := by - rintro S₁ ⟨s₁, t₁, h₁, rfl⟩ S₂ ⟨s₂, t₂, h₂, rfl⟩ hst_nonempty +@[simp] +theorem mem_squareCylinders (C : ∀ i, Set (Set (α i))) (hC : ∀ i, Nonempty (C i)) (S : _) : + S ∈ squareCylinders C ↔ ∃ (s t : _) (_ : ∀ i ∈ s, t i ∈ C i), S = squareCylinder s t := by + simp_rw [squareCylinders_eq_iUnion_image, squareCylinder] + refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩ + · simp only [mem_iUnion, mem_image, mem_pi, mem_univ, forall_const] at h + obtain ⟨s, t, h₀, h₁⟩ := h + use s, t + simp only [h₁, h₀, implies_true, exists_const] + · obtain ⟨s, t, h₀, rfl⟩ := h + simp only [mem_iUnion, mem_image, mem_pi, mem_univ, forall_const] + classical + use s, (fun i ↦ if i ∈ s.toSet then t i else (hC i).some) + refine ⟨fun i ↦ ?_ ,?_⟩ + · by_cases h : i ∈ s <;> simp only [Finset.mem_coe, h, ↓reduceIte, Subtype.coe_prop, h₀] + · refine Set.pi_congr rfl (fun i hi ↦ by simp only [hi, ↓reduceIte] at *) + +theorem squareCylinders_subset_pi (C : ∀ i, Set (Set (α i))) (hC : ∀ i, univ ∈ C i) : + squareCylinders C ⊆ univ.pi '' univ.pi C := by + intro S hS + obtain ⟨s, t, h₀, h₁⟩ := hS + simp only [squareCylinder, mem_pi, mem_univ, forall_const] at h₀ h₁ + classical + use fun i ↦ (if i ∈ s.toSet then (t i) else univ) + refine ⟨fun i ↦ ?_, ?_⟩ + · simp only [mem_pi, mem_univ, forall_const] + by_cases hi : i ∈ s.toSet <;> simp only [hi, ↓reduceIte] + · exact h₀ i + · exact hC i + · rw [h₁, univ_pi_ite s t] + +theorem isPiSystem_squareCylinders [∀ i, Inhabited (α i)] {C : ∀ i, Set (Set (α i))} + (hC : ∀ i, IsPiSystem (C i)) (hC_univ : ∀ i, univ ∈ C i) : IsPiSystem (squareCylinders C) := by classical + haveI h_nempty : ∀ i, Nonempty (C i) := fun i ↦ Nonempty.intro ⟨Set.univ, hC_univ i⟩ + rintro S₁ ⟨s₁, t₁, h₁, rfl⟩ S₂ ⟨s₂, t₂, h₂, rfl⟩ hst_nonempty let t₁' := s₁.piecewise t₁ (fun i ↦ univ) + simp only [Set.mem_pi, Set.mem_univ, forall_const] at h₁ h₂ + have ht₁ (i : ι) : t₁' i ∈ C i := by + by_cases h : i ∈ s₁ + · simp only [h, Finset.piecewise_eq_of_mem, t₁'] + exact h₁ i + · simp only [t₁'] + rw [Finset.piecewise_eq_of_notMem s₁ t₁ (fun i ↦ univ) h] + exact hC_univ i let t₂' := s₂.piecewise t₂ (fun i ↦ univ) - have h1 : ∀ i ∈ (s₁ : Set ι), t₁ i = t₁' i := - fun i hi ↦ (Finset.piecewise_eq_of_mem _ _ _ hi).symm - have h1' : ∀ i ∉ (s₁ : Set ι), t₁' i = univ := - fun i hi ↦ Finset.piecewise_eq_of_notMem _ _ _ hi - have h2 : ∀ i ∈ (s₂ : Set ι), t₂ i = t₂' i := - fun i hi ↦ (Finset.piecewise_eq_of_mem _ _ _ hi).symm - have h2' : ∀ i ∉ (s₂ : Set ι), t₂' i = univ := - fun i hi ↦ Finset.piecewise_eq_of_notMem _ _ _ hi - rw [Set.pi_congr rfl h1, Set.pi_congr rfl h2, ← union_pi_inter h1' h2'] - refine ⟨s₁ ∪ s₂, fun i ↦ t₁' i ∩ t₂' i, ?_, ?_⟩ - · rw [mem_univ_pi] - intro i - have : (t₁' i ∩ t₂' i).Nonempty := by - obtain ⟨f, hf⟩ := hst_nonempty - rw [Set.pi_congr rfl h1, Set.pi_congr rfl h2, mem_inter_iff, mem_pi, mem_pi] at hf - refine ⟨f i, ⟨?_, ?_⟩⟩ - · by_cases hi₁ : i ∈ s₁ - · exact hf.1 i hi₁ - · rw [h1' i hi₁] - exact mem_univ _ - · by_cases hi₂ : i ∈ s₂ - · exact hf.2 i hi₂ - · rw [h2' i hi₂] - exact mem_univ _ - refine hC i _ ?_ _ ?_ this - · by_cases hi₁ : i ∈ s₁ - · rw [← h1 i hi₁] - exact h₁ i (mem_univ _) - · rw [h1' i hi₁] - exact hC_univ i - · by_cases hi₂ : i ∈ s₂ - · rw [← h2 i hi₂] - exact h₂ i (mem_univ _) - · rw [h2' i hi₂] - exact hC_univ i - · rw [Finset.coe_union] + have ht₂ (i : ι) : t₂' i ∈ C i := by + by_cases h : i ∈ s₂ + · simp only [h, Finset.piecewise_eq_of_mem, t₂'] + exact h₂ i + · simp only [t₂'] + rw [Finset.piecewise_eq_of_notMem s₂ t₂ (fun i ↦ univ) h] + exact hC_univ i + have h₁ : (s₁ : Set ι).pi t₁' = (s₁ : Set ι).pi t₁ := by + refine Set.pi_congr rfl ?_ + exact fun i a ↦ (s₁.piecewise_eq_of_mem t₁ (fun i ↦ Set.univ) a) + have h₂ : (s₂ : Set ι).pi t₂' = (s₂ : Set ι).pi t₂ := by + refine Set.pi_congr rfl ?_ + exact fun i a ↦ (s₂.piecewise_eq_of_mem t₂ (fun i ↦ Set.univ) a) + have h : squareCylinder s₁ t₁ ∩ squareCylinder s₂ t₂ = squareCylinder (s₁ ∪ s₂) + (fun i ↦ t₁' i ∩ t₂' i) := by + rw [squareCylinder, squareCylinder, squareCylinder, Finset.coe_union, union_pi_inter, h₁, h₂] + <;> + exact fun i a ↦ Finset.piecewise_eq_of_notMem _ _ (fun i ↦ Set.univ) a + rw [h] at hst_nonempty ⊢ + rw [squareCylinder, squareCylinders_eq_iUnion_image' C, mem_iUnion] + · use (s₁ ∪ s₂), (fun i ↦ t₁' i ∩ t₂' i) + refine ⟨?_, rfl⟩ + apply fun i _ ↦ hC i (t₁' i) (ht₁ i) (t₂' i) (ht₂ i) _ + intro i hi + rw [squareCylinder, pi_nonempty_iff'] at hst_nonempty + exact hst_nonempty i hi + · assumption theorem comap_eval_le_generateFrom_squareCylinders_singleton (α : ι → Type*) [m : ∀ i, MeasurableSpace (α i)] (i : ι) : @@ -124,7 +171,7 @@ theorem comap_eval_le_generateFrom_squareCylinders_singleton · simp only [hji, not_false_iff, dif_neg, MeasurableSet.univ] · simp only [id_eq, eq_mpr_eq_cast, ← h] ext1 x - simp only [singleton_pi, Function.eval, cast_eq, dite_eq_ite, ite_true, mem_preimage] + simp only [singleton_pi, Function.eval, cast_eq, dite_eq_ite, ite_true, Set.mem_preimage] /-- The square cylinders formed from measurable sets generate the product σ-algebra. -/ theorem generateFrom_squareCylinders [∀ i, MeasurableSpace (α i)] : @@ -349,6 +396,33 @@ theorem diff_mem_measurableCylinders (hs : s ∈ measurableCylinders α) rw [diff_eq_compl_inter] exact inter_mem_measurableCylinders (compl_mem_measurableCylinders ht) hs + +section MeasurableCylinders + +lemma isSetAlgebra_measurableCylinders : IsSetAlgebra (measurableCylinders α) where + empty_mem := empty_mem_measurableCylinders α + compl_mem _ := compl_mem_measurableCylinders + union_mem _ _ := union_mem_measurableCylinders + +lemma isSetRing_measurableCylinders : IsSetRing (measurableCylinders α) := + isSetAlgebra_measurableCylinders.isSetRing + +lemma isSetSemiring_measurableCylinders : MeasureTheory.IsSetSemiring (measurableCylinders α) := + isSetRing_measurableCylinders.isSetSemiring + +end MeasurableCylinders + + +theorem iUnion_le_mem_measurableCylinders {s : ℕ → Set (∀ i : ι, α i)} + (hs : ∀ n, s n ∈ measurableCylinders α) (n : ℕ) : + (⋃ i ≤ n, s i) ∈ measurableCylinders α := + isSetRing_measurableCylinders.iUnion_le_mem hs n + +theorem iInter_le_mem_measurableCylinders {s : ℕ → Set (∀ i : ι, α i)} + (hs : ∀ n, s n ∈ measurableCylinders α) (n : ℕ) : + (⋂ i ≤ n, s i) ∈ measurableCylinders α := + isSetRing_measurableCylinders.iInter_le_mem hs n + /-- The measurable cylinders generate the product σ-algebra. -/ theorem generateFrom_measurableCylinders : MeasurableSpace.generateFrom (measurableCylinders α) = MeasurableSpace.pi := by @@ -457,4 +531,5 @@ lemma measurable_restrict_cylinderEvents (Δ : Set ι) : rw [@measurable_pi_iff]; exact fun i ↦ measurable_cylinderEvent_apply i.2 end cylinderEvents + end MeasureTheory diff --git a/Mathlib/MeasureTheory/Constructions/ProjectiveFamilyContent.lean b/Mathlib/MeasureTheory/Constructions/ProjectiveFamilyContent.lean index d198a0f5f15ae4..c424fbb7fb7855 100644 --- a/Mathlib/MeasureTheory/Constructions/ProjectiveFamilyContent.lean +++ b/Mathlib/MeasureTheory/Constructions/ProjectiveFamilyContent.lean @@ -5,7 +5,6 @@ Authors: Rémy Degenne, Peter Pfaffelhuber -/ import Mathlib.MeasureTheory.Constructions.Projective import Mathlib.MeasureTheory.Measure.AddContent -import Mathlib.MeasureTheory.SetAlgebra /-! # Additive content built from a projective family of measures @@ -43,21 +42,6 @@ variable {ι : Type*} {α : ι → Type*} {mα : ∀ i, MeasurableSpace (α i)} {P : ∀ J : Finset ι, Measure (Π j : J, α j)} {s t : Set (Π i, α i)} {I : Finset ι} {S : Set (Π i : I, α i)} -section MeasurableCylinders - -lemma isSetAlgebra_measurableCylinders : IsSetAlgebra (measurableCylinders α) where - empty_mem := empty_mem_measurableCylinders α - compl_mem _ := compl_mem_measurableCylinders - union_mem _ _ := union_mem_measurableCylinders - -lemma isSetRing_measurableCylinders : IsSetRing (measurableCylinders α) := - isSetAlgebra_measurableCylinders.isSetRing - -lemma isSetSemiring_measurableCylinders : MeasureTheory.IsSetSemiring (measurableCylinders α) := - isSetRing_measurableCylinders.isSetSemiring - -end MeasurableCylinders - section ProjectiveFamilyFun open Classical in diff --git a/Mathlib/Topology/Compactness/CompactSystem.lean b/Mathlib/Topology/Compactness/CompactSystem.lean index dd520e7a1026e4..d84700594ff1ab 100644 --- a/Mathlib/Topology/Compactness/CompactSystem.lean +++ b/Mathlib/Topology/Compactness/CompactSystem.lean @@ -4,8 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Rémy Degenne, Peter Pfaffelhuber -/ import Mathlib.Data.Set.Dissipate +import Mathlib.Logic.IsEmpty +import Mathlib.MeasureTheory.Constructions.Cylinders +import Mathlib.Order.OmegaCompletePartialOrder import Mathlib.Topology.Separation.Hausdorff - /-! # Compact systems. @@ -23,9 +25,11 @@ 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.closedCompactSquareCylinders`: Closed and compact square cylinders form a + compact system. -/ -open Set Finset Nat +open Set Nat MeasureTheory variable {α : Type*} {p : Set α → Prop} {C : ℕ → Set α} @@ -261,6 +265,11 @@ theorem of_isCompact_isClosed : · simp only [ne_eq, coe_setOf, nonempty_subtype, not_exists, not_not, s'] at h simp [s', h] +theorem nonempty_isCompactIsClosed : Nonempty { t : Set α | IsCompact t ∧ IsClosed t } := by + simp only [coe_setOf, nonempty_subtype] + use ∅ + simp + /-- 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 @@ -277,4 +286,96 @@ theorem of_isCompact [T2Space α] : end IsCompactIsClosed +section pi + +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 [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] + +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 + +theorem squareCylinders (C : (i : ι) → Set (Set (α i))) (hC₀ : ∀ i, IsCompactSystem (C i)) + (hC₁ : ∀ i, Nonempty (C i)) : + IsCompactSystem (squareCylinders C) := by + apply IsCompactSystem.mono (pi _ (fun i ↦ iff_isCompactSystem_of_or_univ.mp (hC₀ i))) + intro S hS + apply squareCylinders_subset_pi _ (fun i ↦ Or.inr rfl) + change S ∈ MeasureTheory.squareCylinders C at hS + rw [mem_squareCylinders C hC₁] at hS + rw [mem_squareCylinders (fun i s ↦ C i s ∨ s = univ) + (fun i ↦ nonempty_subtype.mpr ⟨univ, Or.inr rfl⟩)] + obtain ⟨s, t, h₀, h₁⟩ := hS + use s, t + simp only [exists_prop] + exact ⟨fun i hi ↦ Or.inl (h₀ i hi), h₁⟩ + +end pi + end IsCompactSystem + +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 MeasureTheory.compactClosedSquareCylinders : Set (Set (Π i, α i)) := + MeasureTheory.squareCylinders (fun i ↦ { t : Set (α i) | IsCompact t ∧ IsClosed t }) + +/-- Products of compact and closed sets form a a compact system. -/ +theorem IsCompactSystem.compactClosedPi : + IsCompactSystem (univ.pi '' univ.pi (fun i ↦ { t : Set (α i) | IsCompact t ∧ IsClosed t })) := + IsCompactSystem.pi _ (fun _ ↦ IsCompactSystem.of_isCompact_isClosed) + +/-- Compact and closed square cylinders are a compact system. -/ +theorem isCompactSystem.compactClosedSquareCylinders : + IsCompactSystem (MeasureTheory.compactClosedSquareCylinders α) := + IsCompactSystem.squareCylinders _ (fun _ ↦ IsCompactSystem.of_isCompact_isClosed) + (fun _ ↦ IsCompactSystem.nonempty_isCompactIsClosed) + +end ClosedCompactSquareCylinders