proposition: Lemma measurableM d1 d2 (T1 : measurableType d1) (T2 : measurableType d2) (A : set T1) (B : set T2) : measurable A -> measurable B -> measurable (A `*` B).
proof: Proof. move=> mA mB. have -> : A `*` B = (A `*` setT) `&` (setT `*` B) :> set (T1 * T2). by rewrite -{1}(setIT A) -{1}(setTI B) setMI. rewrite setMT setTM; apply: measurableI. - by apply: sub_sigma_algebra; left; exists A => //; rewrite setTI. - by apply: sub_sigma_algebra; right; exists B => //; rewrite setTI. Qed.
imports: mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop ) reals ereal signed topology normedtype sequences esum numfun HB(structures)