measurable_tProd_mk — Mathlib

English

The finite product over a list l of indices is measurable when each component set is measurable.

Русский

Пусть есть список индексов l; если каждый множество s_i измеримо, то т-prod по l измерим.

LaTeX

$$$\\mathrm{MeasurableSet}(\\mathrm{Set}.\\mathrm{tprod}\\ l\ \ s)$$$

Lean4

theorem measurable_tProd_mk (l : List δ) : Measurable (@TProd.mk δ X l) := by
  induction l with
  | nil => exact measurable_const
  | cons i l ih => exact (measurable_pi_apply i).prodMk ih

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