source
def IsCompactSystem {α : Type u_1} (p : Set α → Prop) :
Prop

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.

Equations

- IsCompactSystem p = ∀ (C : ℕ → Set α), (∀ (i : ℕ), p (C i)) → ⋂ (i : ℕ), C i = ∅ → ∃ (s : Finset ℕ), ⋂ i ∈ s, C i = ∅

Instances For

source
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 = ∅) :
Finset ℕ

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

Instances For

source
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 ∈ hp.support hC hC_empty, C i = ∅

We prove that the `closedCompactCylinders` are a compact system.

source
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 ⋯)

Instances For

source
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
source
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 ⋯
source
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 ⋯

Instances For

source
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 ⋯
source
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
source
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
source
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 ⋯

Instances For

source
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 ⋯
source
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
source
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
source
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
source
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)
source
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.

Instances For

source
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 ⋯
source
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)
source
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 ⋯
source
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)
source
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
source
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
source
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
source
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
source
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 = ∅
source
theorem isCompactSystem_closedCompactCylinders {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → TopologicalSpace (α i)] :
IsCompactSystem (MeasureTheory.closedCompactCylinders α)

The `closedCompactCylinders` are a compact system.