measurable_updateFinset_left — Mathlib

English

The function updating the left coordinate of a product over a Finset is measurable.

Русский

Функция обновления левой координаты произведения по конечному набору измерима.

LaTeX

$$$\operatorname{Measurable}(\lambda x: \text{updateFinset} x s)$$$

Lean4

@[measurability, fun_prop]
theorem measurable_updateFinset_left [DecidableEq δ] {s : Finset δ} {x : Π i : s, X i} :
    Measurable (updateFinset · s x) :=
  measurable_updateFinset'.comp measurable_prodMk_right

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