English
The measurable cylinders generate the product sigma-algebra.
Русский
Измеримые цилиндры порождают произведение сигма-алгебр.
LaTeX
$$$ \\mathrm{generateFrom}(\\mathrm{measurableCylinders}(\\alpha)) = \\mathrm{pi\\-space} $.$$
Lean4
/-- The measurable cylinders generate the product σ-algebra. -/
theorem generateFrom_measurableCylinders : MeasurableSpace.generateFrom (measurableCylinders α) = MeasurableSpace.pi :=
by
apply le_antisymm
· refine MeasurableSpace.generateFrom_le (fun S hS ↦ ?_)
obtain ⟨s, S, hSm, rfl⟩ := (mem_measurableCylinders _).mp hS
exact hSm.cylinder
· refine iSup_le fun i ↦ ?_
refine (comap_eval_le_generateFrom_squareCylinders_singleton α i).trans ?_
refine MeasurableSpace.generateFrom_mono (fun x ↦ ?_)
simp only [singleton_pi, mem_image, mem_pi, mem_univ, mem_setOf_eq, forall_true_left, mem_measurableCylinders,
forall_exists_index, and_imp]
rintro t ht rfl
refine ⟨{ i }, {f | f ⟨i, Finset.mem_singleton_self i⟩ ∈ t i}, measurable_pi_apply _ (ht i), ?_⟩
ext1 x
simp only [mem_preimage, Function.eval, mem_cylinder, mem_setOf_eq, Finset.restrict]
