English
The product of generated σ-algebras equals the σ-algebra generated by boxes, when the countable spanning condition holds.
Русский
Произведение сгенерированных σ-алгебр равно σ-алгебре, порождаемой коробками, при условии счетного покрытия.
LaTeX
$$$\\mathrm{generateFrom}(\\pi univ '' \\pi univ C) = \\mathrm{pi}$$$
Lean4
/-- If `C` and `D` generate the σ-algebras on `α` resp. `β`, then rectangles formed by `C` and `D`
generate the σ-algebra on `α × β`. -/
theorem generateFrom_eq_pi [h : ∀ i, MeasurableSpace (α i)] {C : ∀ i, Set (Set (α i))}
(hC : ∀ i, generateFrom (C i) = h i) (h2C : ∀ i, IsCountablySpanning (C i)) :
generateFrom (pi univ '' pi univ C) = MeasurableSpace.pi := by simp only [← funext hC, generateFrom_pi_eq h2C]
