← Mathematical handbook

theorem Verification.measurePreserving_product_regroup {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure β) [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν] : MeasureTheory.MeasurePreserving (fun (p : (α × β) × α × β) => ((p.1.1, p.2.1), p.1.2, p.2.2)) ((μ.prod ν).prod (μ.prod ν)) ((μ.prod μ).prod (ν.prod ν))