Theorems · Theorem · measure theory

generateFrom_eq_prod

∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {C : Set (Set α)}
  {D : Set (Set β)},
  MeasurableSpace.generateFrom C = inst →
    MeasurableSpace.generateFrom D = inst_1 →
      IsCountablySpanning C →
        IsCountablySpanning D →
          MeasurableSpace.generateFrom (Set.image2 (fun x1 x2 => x1 ×ˢ x2) C D) = Prod.instMeasurableSpace

If C and D generate the σ-algebras on α resp. β, then rectangles formed by C and D generate the σ-algebra on α × β.

Defined in

Mathlib.MeasureTheory.MeasurableSpace.Prod

Cited by

5 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceMeasurableSpace