cylinderEvents_univ — Mathlib

English

When Δ is the whole index set, the cylinder sigma-algebra equals the product sigma-algebra on the product spaces, i.e., cylinderEvents(univ) = MeasurableSpace.pi.

Русский

Когда Δ представляет собой всё множество индексов, σ-алгебра цилиндров равна произведению σ-алгебр на произведении пространств: cylinderEvents(univ) = MeasurableSpace.pi.

LaTeX

$$$\\mathrm{cylinderEvents}(\\mathrm{univ}) = \\mathrm{MeasurableSpace.pi}$$$

Lean4

@[simp]
theorem cylinderEvents_univ : cylinderEvents (X := X) univ = MeasurableSpace.pi := by
  simp [cylinderEvents, MeasurableSpace.pi]

Похожие утверждения