English
For spaces indexed by natural numbers, measurable cylinders can be described as depending on the first coordinates.
Русский
Для пространств, индексированных по натуральным числам, измеримые цилиндры зависят от первых координат.
LaTeX
$$$ \\mathrm{measurableCylinders}(X) = \\bigcup_{a} \\bigcup_{S} \\{\\mathrm{cylinder}(\\mathrm{Finset.Iic}\\ a, S)\\} $$$
Lean4
/-- The cylinders of a product space indexed by `ℕ` can be seen as depending on the first
coordinates. -/
theorem measurableCylinders_nat {X : ℕ → Type*} [∀ n, MeasurableSpace (X n)] :
measurableCylinders X = ⋃ (a) (S) (_ : MeasurableSet S), {cylinder (Finset.Iic a) S} :=
by
ext s
simp only [mem_measurableCylinders, exists_prop, mem_iUnion]
refine ⟨?_, fun ⟨N, S, mS, s_eq⟩ ↦ ⟨Finset.Iic N, S, mS, s_eq⟩⟩
rintro ⟨t, S, mS, rfl⟩
refine ⟨t.sup id, Finset.restrict₂ t.subset_Iic_sup_id ⁻¹' S, Finset.measurable_restrict₂ _ mS, ?_⟩
unfold cylinder
rw [← preimage_comp, Finset.restrict₂_comp_restrict]
exact mem_singleton _
