measurable_updateFinset — Mathlib

English

The map updating a Finset of coordinates is always measurable.

Русский

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

LaTeX

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

Lean4

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

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