theorem mem_congr_of_measurableSet_cylinderEvents {S : Type u_1} {E : Type u_2} {mE : MeasurableSpace E} {Δ : Set S} {B : Set (S → E)} (hB : MeasurableSet B) {f₁ f₂ : S → E} (h : ∀ i ∈ Δ, f₁ i = f₂ i) : f₁ ∈ B ↔ f₂ ∈ B

theorem MeasureTheory.cylinderEvents_eq_comap_domRestrict {ι : Type u_3} {X : ι → Type u_4} [(i : ι) → MeasurableSpace (X i)] (Δ : Set ι) : cylinderEvents Δ = MeasurableSpace.comap Δ.domRestrict inferInstance

theorem MeasureTheory.cylinderEvents_eq_comap_finsetRestrict {ι : Type u_3} {X : ι → Type u_4} [(i : ι) → MeasurableSpace (X i)] (Λ : Finset ι) : cylinderEvents ↑Λ = MeasurableSpace.comap Λ.restrict inferInstance

theorem Measurable.dependsOn_of_cylinderEvents {ι : Type u_3} {X : ι → Type u_4} [(i : ι) → MeasurableSpace (X i)] {Δ : Set ι} {Z : Type u_5} [MeasurableSpace Z] {f : ((i : ι) → X i) → Z} [MeasurableSingletonClass Z] (hf : Measurable f) : DependsOn f Δ

theorem Measurable.cylinderEvents_of_dependsOn {ι : Type u_3} {X : ι → Type u_4} [(i : ι) → MeasurableSpace (X i)] {Δ : Set ι} {Z : Type u_5} [MeasurableSpace Z] {f : ((i : ι) → X i) → Z} (hf : Measurable f) (hdep : DependsOn f Δ) : Measurable f

theorem MeasureTheory.measurable_cylinderEvents_iff_dependsOn {ι : Type u_3} {X : ι → Type u_4} [(i : ι) → MeasurableSpace (X i)] {Δ : Set ι} {Z : Type u_5} [MeasurableSpace Z] {f : ((i : ι) → X i) → Z} [MeasurableSingletonClass Z] : Measurable f ↔ Measurable f ∧ DependsOn f Δ

@[reducible, inline]

abbrev MeasureTheory.measurableSquareCylinders (ι : Type u_3) (X : ι → Type u_4) [(i : ι) → MeasurableSpace (X i)] : Set (Set ((i : ι) → X i))

Equations

• MeasureTheory.measurableSquareCylinders ι X = MeasureTheory.squareCylinders fun (x : ι) => {s : Set (X x) | MeasurableSet s}

theorem MeasureTheory.IsPiSystem.measurableSquareCylinders {ι : Type u_3} {X : ι → Type u_4} [(i : ι) → MeasurableSpace (X i)] : IsPiSystem (measurableSquareCylinders ι X)

theorem MeasureTheory.generateFrom_measurableSquareCylinders {ι : Type u_3} {X : ι → Type u_4} [(i : ι) → MeasurableSpace (X i)] : MeasurableSpace.generateFrom (measurableSquareCylinders ι X) = MeasurableSpace.pi

theorem MeasureTheory.univ_mem_measurableSquareCylinders {ι : Type u_3} {X : ι → Type u_4} [(i : ι) → MeasurableSpace (X i)] : Set.univ ∈ measurableSquareCylinders ι X

theorem MeasurableSet.pi_cylinderEvents {ι : Type u_3} {X : ι → Type u_4} [(i : ι) → MeasurableSpace (X i)] {Δ s : Set ι} (hs : s ⊆ Δ) (hsc : s.Countable) {t : (i : ι) → Set (X i)} (ht : ∀ i ∈ s, MeasurableSet (t i)) : MeasurableSet (s.pi t)