measurable_restrict_cylinderEvents

English

The restriction map restrict Δ from the full product to the subspace Δ is measurable with respect to cylinderEvents Δ.

Русский

Ограничение restrict Δ с полного произведения на подпространство Δ измеримо относительно cylinderEvents Δ.

LaTeX

$$$\\text{measurable\\_restrict\\_cylinderEvents}(\\Delta) : Measurable[cylinderEvents (X := X) \\Delta] (\\mathrm{restrict}_{\\Delta})$$$

Lean4

theorem measurable_restrict_cylinderEvents (Δ : Set ι) : Measurable[cylinderEvents (X := X) Δ] (restrict Δ) := by
  rw [@measurable_pi_iff]; exact fun i ↦ measurable_cylinderEvent_apply i.2

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