Kolmogorov extension for Boolean coordinates

A consistent family of probability laws on the finite coordinate sets of ι → Bool has a projective limit, for an arbitrary index type ι. The cylinders of ι → Bool are compact and clopen, so the content of the family is σ-additive on the cylinder algebra, and Carathéodory's construction extends it.

theorem Erdos111.isClosed_of_mem_measurableCylinders {ι : Type u_1} {s : Set (ι → Bool)} (hs : s ∈ MeasureTheory.measurableCylinders fun (x : ι) => Bool) : IsClosed s

A measurable cylinder of ι → Bool is closed in the product topology.

theorem Erdos111.exists_isProjectiveLimit_bool {ι : Type u_1} (P : (J : Finset ι) → MeasureTheory.Measure (↥J → Bool)) [∀ (J : Finset ι), MeasureTheory.IsProbabilityMeasure (P J)] (hP : MeasureTheory.IsProjectiveMeasureFamily P) : ∃ (μ : MeasureTheory.Measure (ι → Bool)), MeasureTheory.IsProbabilityMeasure μ ∧ MeasureTheory.IsProjectiveLimit μ P

Kolmogorov extension for Boolean coordinates.