English
The map that updates the i-th coordinate of a function f, sending (f,i) to the updated function, is measurable from the product cylinderEvents Δ × X_i to the cylinder space.
Русский
Отображение обновления i-й координаты функции f измеримо из пространства произведения cylinderEvents Δ × X_i в пространство цилиндров.
LaTeX
$$$\\text{measurable\\_update\\_cylinderEvents'}\\ :\\ @Measurable\\_{·} \\bigl.(cylinderEvents(\\Delta)\\bigr) (update\\; p.1\\; i\\; p.2)$$$
Lean4
/-- The function `(f, x) ↦ update f a x : (Π a, X a) × X a → Π a, X a` is measurable. -/
theorem measurable_update_cylinderEvents' [DecidableEq ι] :
@Measurable _ _ (.prod (cylinderEvents Δ) (m i)) (cylinderEvents Δ) (fun p : (∀ i, X i) × X i ↦ update p.1 i p.2) :=
by
rw [measurable_cylinderEvents_iff]
intro j hj
dsimp [update]
split_ifs with h
· subst h
dsimp
exact measurable_snd
· exact measurable_cylinderEvents_iff.1 measurable_fst hj
