English
The map p ↦ update p.1 a p.2 from (∀ i, X i) × X a to (∀ i, X i) is measurable when δ is countable or under appropriate measurability assumptions.
Русский
Отображение p ↦ update p.1 a p.2 из (∀ i, X i) × X a в (∀ i, X i) измеримо при подходящих предположениях.
LaTeX
$$$\operatorname{Measurable}(\lambda p: (\forall i, X i) \times X a. \; \mathrm{update}\; p.1\ a\ p.2)$$$
Lean4
/-- The function `(f, x) ↦ update f a x : (Π a, X a) × X a → Π a, X a` is measurable. -/
@[measurability, fun_prop]
theorem measurable_update' {a : δ} [DecidableEq δ] : Measurable (fun p : (∀ i, X i) × X a ↦ update p.1 a p.2) :=
by
rw [measurable_pi_iff]
intro j
dsimp [update]
split_ifs with h
· subst h
dsimp
exact measurable_snd
· exact measurable_pi_iff.1 measurable_fst _
