The join of two σ-algebras is generated by intersections

For σ-algebras mF and mG on the same type, the sets tF ∩ tG with tF measurable for mF and tG measurable for mG form a π-system generating the join mF ⊔ mG. Statements about a join, such as independence or conditional independence of mF ⊔ mG from a third σ-algebra, are checked on this π-system.

theorem MeasurableSpace.isPiSystem_inter_measurableSet {Ω : Type u_1} (mF mG : MeasurableSpace Ω) : IsPiSystem {s : Set Ω | ∃ (tF : Set Ω) (tG : Set Ω), MeasurableSet tF ∧ MeasurableSet tG ∧ s = tF ∩ tG}

The sets tF ∩ tG, with tF being mF-measurable and tG being mG-measurable, form a π-system.

theorem MeasurableSpace.sup_eq_generateFrom_inter_measurableSet {Ω : Type u_1} (mF mG : MeasurableSpace Ω) : mF ⊔ mG = generateFrom {s : Set Ω | ∃ (tF : Set Ω) (tG : Set Ω), MeasurableSet tF ∧ MeasurableSet tG ∧ s = tF ∩ tG}

The join mF ⊔ mG is generated by the sets tF ∩ tG with tF being mF-measurable and tG being mG-measurable.

theorem MeasurableSpace.exists_eq_preimage_pi_of_mem_piiUnionInter {Ω : Type u_1} {ι : Type u_2} {α : Type u_3} [MeasurableSpace α] {X : ι → Ω → α} {S : Set ι} {A : Set Ω} (hA : A ∈ piiUnionInter (fun (p : ι) => {s : Set Ω | MeasurableSet s}) S) : ∃ (t : Finset ι) (C : ι → Set α), ↑t ⊆ S ∧ (∀ p ∈ t, MeasurableSet (C p)) ∧ A = (fun (ω : Ω) (p : ι) => X p ω) ⁻¹' (↑t).pi C

A cylinder of the block over S is the preimage, under the map ω ↦ (X p ω)ₚ, of a measurable cylinder over a finite subset of S: this describes the members of piiUnionInter of the comap σ-algebras.