cylinderEvents_le_pi — Mathlib

English

For any Δ, the cylinder sigma-algebra on Δ is contained in the product sigma-algebra: cylinderEvents(Δ) ≤ MeasurableSpace.pi.

Русский

Для любого Δ цилиндровая σ-алгебра удовлетворяет cylinderEvents(Δ) ⊆ MeasurableSpace.pi.

LaTeX

$$$\\mathrm{cylinderEvents}(\\Delta) \\le \\mathrm{MeasurableSpace.pi}$$$

Lean4

theorem cylinderEvents_le_pi : cylinderEvents (X := X) Δ ≤ MeasurableSpace.pi := by
  simpa using cylinderEvents_mono (subset_univ _)

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