A compact system of square cylinders #
Compact closed square cylinders form a compact system
(isCompactSystem_compactClosedSquareCylinders), hence so do the countable intersections of finite
unions of them. We show that every cylinder with a compact closed base belongs to that compact
system. This is used in the proof of the Kolmogorov extension theorem, to approximate measurable
cylinders from inside by sets of a compact system.
Main statements #
isCompactSystem_countableInfClosure_supClosure_compactClosedSquareCylinders: countable intersections of finite unions of compact closed square cylinders form a compact system.cylinder_mem_countableInfClosure_supClosure: in a product of second-countable R₁ spaces, a cylinder with a compact closed base is a countable intersection of finite unions of compact closed square cylinders.
theorem
cylinder_univ_pi_mem_compactClosedSquareCylinders
{ι : Type u_1}
{α : ι → Type u_2}
[(i : ι) → TopologicalSpace (α i)]
{J : Finset ι}
{t : (j : ↥J) → Set (α ↑j)}
(ht_compact : ∀ (j : ↥J), IsCompact (t j))
(ht_closed : ∀ (j : ↥J), IsClosed (t j))
:
A cylinder whose base is a product of compact closed sets is a compact closed square cylinder.
theorem
isCompactSystem_countableInfClosure_supClosure_compactClosedSquareCylinders
{ι : Type u_1}
{α : ι → Type u_2}
[(i : ι) → TopologicalSpace (α i)]
:
Countable intersections of finite unions of compact closed square cylinders (and of ∅)
form a compact system.
theorem
cylinder_mem_countableInfClosure_supClosure
{ι : Type u_1}
{α : ι → Type u_2}
[(i : ι) → TopologicalSpace (α i)]
[∀ (i : ι), SecondCountableTopology (α i)]
[∀ (i : ι), R1Space (α i)]
{J : Finset ι}
{K : Set ((j : ↥J) → α ↑j)}
(hK_compact : IsCompact K)
(hK_closed : IsClosed K)
:
A cylinder with a compact closed base is a countable intersection of finite unions of compact closed square cylinders.