proposition: Lemma measurable_prod_measurableType : (d1, d2).-prod.-measurable = <<s M1xM2 >>.
proof: Proof. rewrite eqEsubset; split. apply: smallest_sub; first exact: smallest_sigma_algebra. rewrite subUset; split. - have /subset_trans : preimage_class setT fst M1 `<=` M1xM2. by move=> _ [X MX <-]; exists X=> //; exists setT; rewrite /M2 // setIC//. by apply; exact: sub_sigma_algebra. - have /subset_trans : preimage_class setT snd M2 `<=` M1xM2. by move=> _ [Y MY <-]; exists setT; rewrite /M1 //; exists Y. by apply; exact: sub_sigma_algebra. apply: smallest_sub; first exact: smallest_sigma_algebra. by move=> _ [A MA] [B MB] <-; apply: measurableM => //; exact: sub_sigma_algebra. 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)