Theorems · Definition · measure theory

MeasureTheory.measurableCylinders

{ι : Type u_2} → (α : ι → Type u_1) → [(i : ι) → MeasurableSpace (α i)] → Set (Set ((i : ι) → α i))

Given a finite set s of indices, a cylinder is the preimage of a set S of ∀ i : s, α i by the projection from ∀ i, α i to ∀ i : s, α i. measurableCylinders is the set of all cylinders with measurable base S.

Defined in

Mathlib.MeasureTheory.Constructions.Cylinders

Cited by

48 results in Mathlib

Foundations

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

Assumes

MeasurableSpace