measurable_cylinderEvents_iff — Mathlib

English

A function g: α → ∀ i, X_i is measurable w.r.t. cylinderEvents Δ iff each coordinate function g_i is measurable whenever i ∈ Δ.

Русский

Функция g: α → ∀ i, X_i измерима относительно cylinderEvents Δ тогда и только тогда, когда каждая координатная функция g_i измерима при условии i ∈ Δ.

LaTeX

$$$@Measurable_{(cylinderEvents \\Delta)}(g) \\iff \\forall i,\\ i \\in \\Delta \\rightarrow Measurable(\\lambda a \\mapsto g(a,i))$$$

Lean4

theorem measurable_cylinderEvents_iff {g : α → ∀ i, X i} :
    @Measurable _ _ _ (cylinderEvents Δ) g ↔ ∀ ⦃i⦄, i ∈ Δ → Measurable fun a ↦ g a i := by
  simp_rw [measurable_iff_comap_le, cylinderEvents, MeasurableSpace.comap_iSup, MeasurableSpace.comap_comp,
    Function.comp_def, iSup_le_iff]

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