measurable_updateFinset' — Mathlib

English

For a finite index set Finset δ, the map updating finitely many coordinates is measurable.

Русский

Для конечного множества индексов обновление конечного числа координат измеримо.

LaTeX

$$$\text{Measurable} (\lambda p: (\Pi i, X i) \times (\Pi i \in s, X i) \mapsto \text{updateFinset} p.1 s p.2)$$$

Lean4

@[measurability, fun_prop]
theorem measurable_updateFinset' [DecidableEq δ] {s : Finset δ} :
    Measurable (fun p : (Π i, X i) × (Π i : s, X i) ↦ updateFinset p.1 s p.2) :=
  by
  simp only [updateFinset, measurable_pi_iff]
  intro i
  by_cases h : i ∈ s <;> simp [h, Measurable.eval, measurable_fst, measurable_snd]

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