English
The product σ-algebra is generated by the square cylinders formed from measurable sets, i.e., generateFrom(squareCylinders) equals pi.
Русский
Произведение σ-алгебр порождается квадратными цилиндрами, образованными из измеримых множеств; порождаемая ими σ-алгебра равна продуктовой.
LaTeX
$$$$\\mathrm{generateFrom}(\\mathrm{squareCylinders}(i \\mapsto \\{s \\mid \\mathrm{MeasurableSet}(s)\\})) = \\mathrm{pi}.$$$$
Lean4
/-- The square cylinders formed from measurable sets generate the product σ-algebra. -/
theorem generateFrom_squareCylinders [∀ i, MeasurableSpace (α i)] :
MeasurableSpace.generateFrom (squareCylinders fun i ↦ {s : Set (α i) | MeasurableSet s}) = MeasurableSpace.pi :=
by
apply le_antisymm
· rw [MeasurableSpace.generateFrom_le_iff]
rintro S ⟨s, t, h, rfl⟩
simp only [mem_univ_pi, mem_setOf_eq] at h
exact MeasurableSet.pi (Finset.countable_toSet _) (fun i _ ↦ h i)
· refine iSup_le fun i ↦ ?_
refine (comap_eval_le_generateFrom_squareCylinders_singleton α i).trans ?_
refine MeasurableSpace.generateFrom_mono ?_
rw [← Finset.coe_singleton, squareCylinders_eq_iUnion_image]
exact
subset_iUnion
(fun (s : Finset ι) ↦ (fun t : ∀ i, Set (α i) ↦ (s : Set ι).pi t) '' univ.pi (fun i ↦ setOf MeasurableSet))
({ i } : Finset ι)
