tProd — Mathlib

English

The finite product of sets over a list l is measurable when each factor is measurable.

Русский

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

LaTeX

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

Lean4

theorem tProd (l : List δ) {s : ∀ i, Set (X i)} (hs : ∀ i, MeasurableSet (s i)) : MeasurableSet (Set.tprod l s) := by
  induction l with
  | nil => exact MeasurableSet.univ
  | cons i l ih => exact (hs i).prod ih

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