univ_pi — Mathlib

English

If δ is countable and each t(i) is a measurable set, then the product over a universal index set is measurable.

Русский

Если δ счётно и каждое t(i) измеримо, то произведение по всем i измеримо.

LaTeX

$$$\\mathrm{MeasurableSet}(\\pi\\,\\text{univ}\\, t)$$$

Lean4

protected theorem univ_pi [Countable δ] {t : ∀ i : δ, Set (X i)} (ht : ∀ i, MeasurableSet (t i)) :
    MeasurableSet (pi univ t) :=
  MeasurableSet.pi (to_countable _) fun i _ => ht i

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