measurable_cylinderEvent_apply — Mathlib

English

For any i with i ∈ Δ, the projection map onto the i-th coordinate is measurable with respect to cylinderEvents Δ.

Русский

Для любого i, удовлетворяющего i ∈ Δ, проекция на i-ю координату измерима относительно cylinderEvents Δ.

LaTeX

$$$\\text{hi}: i \\in \\Delta \\Rightarrow \\text{Measurable}_{cylinderEvents(\\Delta)}(\\lambda f:\\\u2200 \\; f\\mapsto f(i))$$$

Lean4

@[fun_prop, aesop safe 100 apply (rule_sets := [Measurable])]
theorem measurable_cylinderEvent_apply (hi : i ∈ Δ) : Measurable[cylinderEvents Δ] fun f : ∀ i, X i => f i :=
  measurable_cylinderEvents_iff.1 measurable_id hi

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