measurable_restrict — Mathlib

English

Let (X_i) be a family of measurable spaces indexed by δ. For any finite subset s ⊆ δ, the projection map that retains only the coordinates in s from the full product ∏_{i ∈ δ} X_i to the finite product ∏_{i ∈ s} X_i is measurable.

Русский

Пусть (X_i) — семейство измеримых пространств, индексируемое множеством δ. Для любого конечного подмножества s ⊆ δ проекция, сохраняющая только координаты из s, из произведения по всем i к произведению по i ∈ s измерима.

LaTeX

$$$p_s: \\prod_{i\\in \\delta} X(i) \\to \\prod_{i\\in s} X(i), \\quad p_s((x_i)_{i\\in \\delta})=(x_i)_{i\\in s}, \\quad \\mathrm{Measurable}(p_s)$$$

Lean4

@[measurability, fun_prop]
theorem measurable_restrict (s : Finset δ) : Measurable (s.restrict (π := X)) :=
  measurable_pi_lambda _ fun _ ↦ measurable_pi_apply _

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