eval_cylinderEvents — Mathlib

English

If g is a measurable function from α to ∀ i, X_i, and i ∈ Δ, then the i-th coordinate evaluation g(a) i is measurable.

Русский

Если g измерима по отношению к цилиндрам, то для любого i ∈ Δ функция a ↦ g(a)_i измерима.

LaTeX

$$$\\text{hi}: i\\in\\Delta,\\; hg:\\ @Measurable _ _ _ (cylinderEvents\\Delta)\\ g\\Rightarrow \\ Measurable(\\lambda a. g(a,i))$$$

Lean4

@[aesop safe 100 apply (rule_sets := [Measurable])]
theorem eval_cylinderEvents {g : α → ∀ i, X i} (hi : i ∈ Δ) (hg : @Measurable _ _ _ (cylinderEvents Δ) g) :
    Measurable fun a ↦ g a i :=
  (measurable_cylinderEvent_apply hi).comp hg

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