Theorems · Theorem · measure theory

MeasureTheory.measurable_cylinderEvents_iff

∀ {α : Type u_1} {ι : Type u_2} {X : ι → Type u_3} {mα : MeasurableSpace α} [m : (i : ι) → MeasurableSpace (X i)]
  {Δ : Set ι} {g : α → (i : ι) → X i}, Measurable g ↔ ∀ ⦃i : ι⦄, i ∈ Δ → Measurable fun a => g a i

Defined in

Mathlib.MeasureTheory.Constructions.Cylinders

Cited by

2 results in Mathlib

Foundations

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

Assumes

MeasurableSpace