English
Let (X_i) be a family of measurable spaces indexed by i in ι, and let Δ be a subset of ι. The cylinder sigma-algebra on the product ∏_i X_i is the smallest sigma-algebra for which every projection onto the i-th coordinate (for i ∈ Δ) is measurable.
Русский
Пусть (X_i) — семейство измеримых множест на индексах i из ι, а Δ ⊆ ι. σ-алгебра цилиндров на произведении ∏_i X_i является минимальной σ-алгеброй, которая делает проекции на i-ю координату измеримыми для всех i ∈ Δ.
LaTeX
$$$\\mathrm{cylinderEvents}(\\Delta) = \\sigma\\bigl\\{ \\pi_i^{-1}(B) \\;|\\; i \\in \\Delta,\\ B \\in \\mathcal{M}_i \\bigr\\}$$$
Lean4
/-- The σ-algebra of cylinder events on `Δ`. It is the smallest σ-algebra making the projections
on the `i`-th coordinate measurable for all `i ∈ Δ`. -/
def cylinderEvents (Δ : Set ι) : MeasurableSpace (∀ i, X i) :=
⨆ i ∈ Δ, (m i).comap fun σ ↦ σ i
