measurable_update — Mathlib

English

The map updating a single coordinate is always measurable.

Русский

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

LaTeX

$$$\operatorname{Measurable}(\text{update } f\ a)$$$

Lean4

/-- The function `update f a : X a → Π a, X a` is always measurable.
  This doesn't require `f` to be measurable.
  This should not be confused with the statement that `update f a x` is measurable. -/
@[measurability, fun_prop]
theorem measurable_update (f : ∀ a : δ, X a) {a : δ} [DecidableEq δ] : Measurable (update f a) :=
  measurable_update'.comp measurable_prodMk_left

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