measurable_update_cylinderEvents_left

English

The map f ↦ update f a x is measurable with respect to cylinderEvents Δ when the right-hand side uses the right projection.

Русский

Отображение f ↦ update f a x измеримо относительно cylinderEvents Δ, если использовать правую проекцию.

LaTeX

$$$\\text{measurable\\_update\\_cylinderEvents left} \\ : \\ Measurable(\\lambda f. (\\text{update}\\, f\, a))$$$

Lean4

theorem measurable_update_cylinderEvents_left {a : ι} [DecidableEq ι] {x : X a} :
    @Measurable _ _ (cylinderEvents Δ) (cylinderEvents Δ) (update · a x) :=
  measurable_update_cylinderEvents'.comp measurable_prodMk_right

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