noncomputable def IsCompactSystem.support {α : Type u_1} {p : Set α → Prop} {C : ℕ → Set α} (hp : IsCompactSystem p) (hC : ∀ (i : ℕ), p (C i)) (hC_empty : ⋂ (i : ℕ), C i = ∅) : ℕ

In a compact system, given a countable family with empty intersection, we choose a finite subfamily with empty intersection

Equations

• hp.support hC hC_empty = ⋯.choose

theorem IsCompactSystem.iInter_eq_empty {α : Type u_1} {p : Set α → Prop} {C : ℕ → Set α} (hp : IsCompactSystem p) (hC : ∀ (i : ℕ), p (C i)) (hC_empty : ⋂ (i : ℕ), C i = ∅) : ⋂ (i : ℕ), ⋂ (_ : i ≤ hp.support hC hC_empty), C i = ∅

We prove that the closedCompactCylinders are a compact system.

def allProj {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → TopologicalSpace (α i)] {s : ℕ → Set ((i : ι) → α i)} (hs : ∀ (n : ℕ), s n ∈ MeasureTheory.closedCompactCylinders α) : Set ι

All indices in ι that are constrained by the condition ∀ n, s n ∈ closedCompactCylinders α. That is, the union of all indices in the bases of the cylinders.

Equations

• allProj hs = ⋃ (n : ℕ), ↑(MeasureTheory.closedCompactCylinders.finset ⋯)

theorem subset_allProj {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → TopologicalSpace (α i)] {s : ℕ → Set ((i : ι) → α i)} (hs : ∀ (n : ℕ), s n ∈ MeasureTheory.closedCompactCylinders α) (n : ℕ) : ↑(MeasureTheory.closedCompactCylinders.finset ⋯) ⊆ allProj hs

theorem exists_nat_proj {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → TopologicalSpace (α i)] {s : ℕ → Set ((i : ι) → α i)} (hs : ∀ (n : ℕ), s n ∈ MeasureTheory.closedCompactCylinders α) (i : ι) (hi : i ∈ allProj hs) : ∃ (n : ℕ), i ∈ MeasureTheory.closedCompactCylinders.finset ⋯

noncomputable def indexProj {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → TopologicalSpace (α i)] {s : ℕ → Set ((i : ι) → α i)} (hs : ∀ (n : ℕ), s n ∈ MeasureTheory.closedCompactCylinders α) (i : ↑(allProj hs)) : ℕ

The smallest n such that i ∈ Js (hs n). That is, the first n such that i belongs to the finset defining the cylinder for s n.

Equations

• indexProj hs i = Nat.find ⋯

theorem mem_indexProj {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → TopologicalSpace (α i)] {s : ℕ → Set ((i : ι) → α i)} (hs : ∀ (n : ℕ), s n ∈ MeasureTheory.closedCompactCylinders α) (i : ↑(allProj hs)) : ↑i ∈ MeasureTheory.closedCompactCylinders.finset ⋯

theorem indexProj_le {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → TopologicalSpace (α i)] {s : ℕ → Set ((i : ι) → α i)} (hs : ∀ (n : ℕ), s n ∈ MeasureTheory.closedCompactCylinders α) (n : ℕ) (i : ↥(MeasureTheory.closedCompactCylinders.finset ⋯)) : indexProj hs ⟨↑i, ⋯⟩ ≤ n

theorem surjective_proj_allProj {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → TopologicalSpace (α i)] {s : ℕ → Set ((i : ι) → α i)} [∀ (i : ι), Nonempty (α i)] (hs : ∀ (n : ℕ), s n ∈ MeasureTheory.closedCompactCylinders α) : Function.Surjective fun (f : (i : ι) → α i) (i : ↑(allProj hs)) => f ↑i

def projCylinder {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → TopologicalSpace (α i)] {s : ℕ → Set ((i : ι) → α i)} (hs : ∀ (n : ℕ), s n ∈ MeasureTheory.closedCompactCylinders α) (n : ℕ) : Set ((i : ↑(allProj hs)) → α ↑i)

Given a countable family of closed cylinders, consider one of them as depending only on the countably many coordinates that appear in all of them.

Equations

• projCylinder hs n = (fun (f : (i : ↑(allProj hs)) → α ↑i) (i : ↥(MeasureTheory.closedCompactCylinders.finset ⋯)) => f ⟨↑i, ⋯⟩) ⁻¹' MeasureTheory.closedCompactCylinders.set ⋯

theorem mem_projCylinder {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → TopologicalSpace (α i)] {s : ℕ → Set ((i : ι) → α i)} (hs : ∀ (n : ℕ), s n ∈ MeasureTheory.closedCompactCylinders α) (n : ℕ) (x : (i : ↑(allProj hs)) → α ↑i) : x ∈ projCylinder hs n ↔ (fun (i : ↥(MeasureTheory.closedCompactCylinders.finset ⋯)) => x ⟨↑i, ⋯⟩) ∈ MeasureTheory.closedCompactCylinders.set ⋯

theorem preimage_projCylinder {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → TopologicalSpace (α i)] {s : ℕ → Set ((i : ι) → α i)} (hs : ∀ (n : ℕ), s n ∈ MeasureTheory.closedCompactCylinders α) (n : ℕ) : (fun (f : (i : ι) → α i) (i : ↑(allProj hs)) => f ↑i) ⁻¹' projCylinder hs n = s n

theorem nonempty_projCylinder {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → TopologicalSpace (α i)] {s : ℕ → Set ((i : ι) → α i)} (hs : ∀ (n : ℕ), s n ∈ MeasureTheory.closedCompactCylinders α) (n : ℕ) (hs_nonempty : (s n).Nonempty) : (projCylinder hs n).Nonempty

theorem nonempty_projCylinder_iff {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → TopologicalSpace (α i)] {s : ℕ → Set ((i : ι) → α i)} [∀ (i : ι), Nonempty (α i)] (hs : ∀ (n : ℕ), s n ∈ MeasureTheory.closedCompactCylinders α) (n : ℕ) : (projCylinder hs n).Nonempty ↔ (s n).Nonempty

theorem isClosed_projCylinder {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → TopologicalSpace (α i)] {s : ℕ → Set ((i : ι) → α i)} (hs : ∀ (n : ℕ), s n ∈ MeasureTheory.closedCompactCylinders α) (hs_closed : ∀ (n : ℕ), IsClosed (MeasureTheory.closedCompactCylinders.set ⋯)) (n : ℕ) : IsClosed (projCylinder hs n)

def piCylinderSet {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → TopologicalSpace (α i)] {s : ℕ → Set ((i : ι) → α i)} (hs : ∀ (n : ℕ), s n ∈ MeasureTheory.closedCompactCylinders α) : Set ((i : ↑(allProj hs)) → α ↑i)

Given countably many closed compact cylinders, the product set which, in each relevant coordinate, is the projection of the first cylinder for which this coordinate is relevant.

Equations

• One or more equations did not get rendered due to their size.

theorem mem_piCylinderSet {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → TopologicalSpace (α i)] {s : ℕ → Set ((i : ι) → α i)} (hs : ∀ (n : ℕ), s n ∈ MeasureTheory.closedCompactCylinders α) (x : (i : ↑(allProj hs)) → α ↑i) : x ∈ piCylinderSet hs ↔ ∀ (i : ↑(allProj hs)), x i ∈ (fun (a : (j : ↥(MeasureTheory.closedCompactCylinders.finset ⋯)) → α ↑j) => a ⟨↑i, ⋯⟩) '' MeasureTheory.closedCompactCylinders.set ⋯

theorem isCompact_piCylinderSet {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → TopologicalSpace (α i)] {s : ℕ → Set ((i : ι) → α i)} (hs : ∀ (n : ℕ), s n ∈ MeasureTheory.closedCompactCylinders α) : IsCompact (piCylinderSet hs)

theorem piCylinderSet_eq_pi_univ {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → TopologicalSpace (α i)] {s : ℕ → Set ((i : ι) → α i)} (hs : ∀ (n : ℕ), s n ∈ MeasureTheory.closedCompactCylinders α) : piCylinderSet hs = Set.univ.pi fun (i : ↑(allProj hs)) => (fun (a : (j : ↥(MeasureTheory.closedCompactCylinders.finset ⋯)) → α ↑j) => a ⟨↑i, ⋯⟩) '' MeasureTheory.closedCompactCylinders.set ⋯

theorem isClosed_piCylinderSet {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → TopologicalSpace (α i)] {s : ℕ → Set ((i : ι) → α i)} (hs : ∀ (n : ℕ), s n ∈ MeasureTheory.closedCompactCylinders α) : IsClosed (piCylinderSet hs)

theorem nonempty_piCylinderSet {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → TopologicalSpace (α i)] {s : ℕ → Set ((i : ι) → α i)} (hs : ∀ (n : ℕ), s n ∈ MeasureTheory.closedCompactCylinders α) (hs_nonempty : ∀ (i : ℕ), (s i).Nonempty) : (piCylinderSet hs).Nonempty

theorem iInter_subset_piCylinderSet {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → TopologicalSpace (α i)] {s : ℕ → Set ((i : ι) → α i)} (hs : ∀ (n : ℕ), s n ∈ MeasureTheory.closedCompactCylinders α) : ⋂ (n : ℕ), projCylinder hs n ⊆ piCylinderSet hs

theorem nonempty_iInter_projCylinder_inter_piCylinderSet {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → TopologicalSpace (α i)] {s : ℕ → Set ((i : ι) → α i)} (hs : ∀ (n : ℕ), s n ∈ MeasureTheory.closedCompactCylinders α) (hs_nonempty : ∀ (i : ℕ), (s i).Nonempty) (h_nonempty : ∀ (n : ℕ), (⋂ (i : ℕ), ⋂ (_ : i ≤ n), projCylinder hs i).Nonempty) (n : ℕ) : ((⋂ (i : ℕ), ⋂ (_ : i ≤ n), projCylinder hs i) ∩ piCylinderSet hs).Nonempty

theorem nonempty_iInter_projCylinder {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → TopologicalSpace (α i)] {s : ℕ → Set ((i : ι) → α i)} (hs : ∀ (n : ℕ), s n ∈ MeasureTheory.closedCompactCylinders α) (hs_nonempty : ∀ (i : ℕ), (s i).Nonempty) (h_nonempty : ∀ (n : ℕ), (⋂ (i : ℕ), ⋂ (_ : i ≤ n), projCylinder hs i).Nonempty) : (⋂ (i : ℕ), projCylinder hs i).Nonempty

theorem exists_finset_iInter_projCylinder_eq_empty {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → TopologicalSpace (α i)] {s : ℕ → Set ((i : ι) → α i)} [∀ (i : ι), Nonempty (α i)] (hs : ∀ (n : ℕ), s n ∈ MeasureTheory.closedCompactCylinders α) (h : ⋂ (n : ℕ), projCylinder hs n = ∅) : ∃ (t : Finset ℕ), ⋂ i ∈ t, projCylinder hs i = ∅

theorem isCompactSystem_closedCompactCylinders {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → TopologicalSpace (α i)] : IsCompactSystem (MeasureTheory.closedCompactCylinders α)

The closedCompactCylinders are a compact system.