Products of discrete σ-algebras

The product of the discrete σ-algebras on two countable types is again discrete. Countability is what makes this work: the measurable rectangles already exhaust the singletons of the product, and countably many of them suffice to build any subset.

Main results

• TauCeti.MeasureTheory.prod_top_eq_top_of_countable: the product of the discrete σ-algebras on two countable types is discrete.

theorem TauCeti.MeasureTheory.prod_top_eq_top_of_countable (α : Type u_1) (β : Type u_2) [Countable α] [Countable β] : ⊤.prod ⊤ = ⊤

The product of the discrete σ-algebras on two countable types is discrete.