English
Let C generate the σ-algebra on α and D generate the σ-algebra on β, and assume both C and D are countably spanning. Then the σ-algebra generated by the rectangles s × t with s ∈ C and t ∈ D is the product σ-algebra on α × β.
Русский
Пусть C порождает σ-алгебру на α и D порождает σ-алгебру на β, причем C и D счётнопокрыты. Тогда σ-алгебра, порожденная прямоугольниками s × t с s ∈ C и t ∈ D, совпадает с произведением σ-алгебр на α × β.
LaTeX
$$$\sigma\bigl(\{ s \times t \mid s \in C,\ t \in D \}\bigr) = \mathcal{M}_α \otimes \mathcal{M}_β$$$
Lean4
/-- If `C` and `D` generate the σ-algebras on `α` resp. `β`, then rectangles formed by `C` and `D`
generate the σ-algebra on `α × β`. -/
theorem generateFrom_eq_prod {C : Set (Set α)} {D : Set (Set β)} (hC : generateFrom C = ‹_›) (hD : generateFrom D = ‹_›)
(h2C : IsCountablySpanning C) (h2D : IsCountablySpanning D) :
generateFrom (image2 (· ×ˢ ·) C D) = Prod.instMeasurableSpace := by rw [← hC, ← hD, generateFrom_prod_eq h2C h2D]
