pi — Mathlib · SciLib

English

If δ is countable and each t(i) is a measurable subset of X(i), then the product set π s t is measurable.

Русский

Пусть индексное множество δ счётно и каждое t(i) является измеримым подмножеством X(i); произведение π s t измеримо.

LaTeX

$$$\\mathrm{MeasurableSet}(\\pi s t)$$$

Lean4

@[measurability]
protected theorem pi {s : Set δ} {t : ∀ i : δ, Set (X i)} (hs : s.Countable) (ht : ∀ i ∈ s, MeasurableSet (t i)) :
    MeasurableSet (s.pi t) := by
  rw [pi_def]
  exact MeasurableSet.biInter hs fun i hi => measurable_pi_apply _ (ht i hi)

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