# Cylinders with closed compact bases #

We define the set of all cylinders with closed compact bases. Those sets play a role in the proof of Kolmogorov's extension theorem.

## Main definitions #

- `closedCompactCylinders X`: the set of all cylinders of `Π i, X i` based on closed compact sets.

## Main statements #

- `mem_measurableCylinders_of_mem_closedCompactCylinders`: in a topological space with second countable topology and measurable open sets, a set in `closedCompactCylinders X` is a measurable cylinder.

source
def MeasureTheory.closedCompactCylinders {ι : Type u_1} (X : ι → Type u_2) [(i : ι) → TopologicalSpace (X i)] :
Set (Set ((i : ι) → X i))

The set of all cylinders based on closed compact sets. Note that such a set is closed, but not compact in general (for instance, the whole space is always a closed compact cylinder).

Equations

- MeasureTheory.closedCompactCylinders X = ⋃ (s : Finset ι), ⋃ (S : Set ((i : ↥s) → X ↑i)), ⋃ (_ : IsClosed S), ⋃ (_ : IsCompact S), {MeasureTheory.cylinder s S}

Instances For

source
theorem MeasureTheory.empty_mem_closedCompactCylinders {ι : Type u_1} (X : ι → Type u_2) [(i : ι) → TopologicalSpace (X i)] :
∅ ∈ closedCompactCylinders X
source
theorem MeasureTheory.mem_closedCompactCylinders {ι : Type u_1} {X : ι → Type u_2} [(i : ι) → TopologicalSpace (X i)] (t : Set ((i : ι) → X i)) :
t ∈ closedCompactCylinders X ↔ ∃ (s : Finset ι) (S : Set ((i : ↥s) → X ↑i)), IsClosed S ∧ IsCompact S ∧ t = cylinder s S
source
noncomputable def MeasureTheory.closedCompactCylinders.finset {ι : Type u_1} {X : ι → Type u_2} [(i : ι) → TopologicalSpace (X i)] {t : Set ((i : ι) → X i)} (ht : t ∈ closedCompactCylinders X) :
Finset ι

A finset `s` such that `t = cylinder s S`. `S` is given by `closedCompactCylinders.set`.

Equations

- MeasureTheory.closedCompactCylinders.finset ht = ⋯.choose

Instances For

source
def MeasureTheory.closedCompactCylinders.set {ι : Type u_1} {X : ι → Type u_2} [(i : ι) → TopologicalSpace (X i)] {t : Set ((i : ι) → X i)} (ht : t ∈ closedCompactCylinders X) :
Set ((i : ↥(finset ht)) → X ↑i)

A set `S` such that `t = cylinder s S`. `s` is given by `closedCompactCylinders.finset`.

Equations

- MeasureTheory.closedCompactCylinders.set ht = ⋯.choose

Instances For

source
theorem MeasureTheory.closedCompactCylinders.isClosed {ι : Type u_1} {X : ι → Type u_2} [(i : ι) → TopologicalSpace (X i)] {t : Set ((i : ι) → X i)} (ht : t ∈ closedCompactCylinders X) :
IsClosed (set ht)
source
theorem MeasureTheory.closedCompactCylinders.isCompact {ι : Type u_1} {X : ι → Type u_2} [(i : ι) → TopologicalSpace (X i)] {t : Set ((i : ι) → X i)} (ht : t ∈ closedCompactCylinders X) :
IsCompact (set ht)
source
theorem MeasureTheory.closedCompactCylinders.eq_cylinder {ι : Type u_1} {X : ι → Type u_2} [(i : ι) → TopologicalSpace (X i)] {t : Set ((i : ι) → X i)} (ht : t ∈ closedCompactCylinders X) :
t = cylinder (finset ht) (set ht)
source
theorem MeasureTheory.cylinder_mem_closedCompactCylinders {ι : Type u_1} {X : ι → Type u_2} [(i : ι) → TopologicalSpace (X i)] (s : Finset ι) (S : Set ((i : ↥s) → X ↑i)) (hS_closed : IsClosed S) (hS_compact : IsCompact S) :
cylinder s S ∈ closedCompactCylinders X
source
theorem MeasureTheory.mem_measurableCylinders_of_mem_closedCompactCylinders {ι : Type u_1} {X : ι → Type u_2} [(i : ι) → TopologicalSpace (X i)] {t : Set ((i : ι) → X i)} [(i : ι) → MeasurableSpace (X i)] [∀ (i : ι), SecondCountableTopology (X i)] [∀ (i : ι), OpensMeasurableSpace (X i)] (ht : t ∈ closedCompactCylinders X) :
t ∈ measurableCylinders X