measurable_restrict₂ — Mathlib

English

Let s ⊆ t be finite subsets of δ. The projection from the t-coordinate product to the s-coordinate product is measurable.

Русский

Пусть s ⊆ t — конечные подмножества множества индексов. Проекция from произведения по t к произведению по s измерима.

LaTeX

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

Lean4

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

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