Theorems · Theorem · measure theory

MeasureTheory.measurableCylinders_nat

∀ {X : ℕ → Type u_1} [inst : (n : ℕ) → MeasurableSpace (X n)],
  MeasureTheory.measurableCylinders X = ⋃ a, ⋃ S, ⋃ (_ : MeasurableSet S), {MeasureTheory.cylinder (Finset.Iic a) S}

The cylinders of a product space indexed by ℕ can be seen as depending on the first coordinates.

Defined in

Mathlib.MeasureTheory.Constructions.Cylinders

Cited by

2 results in Mathlib

Foundations

Depth 72 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MeasurableSpace