proposition: Lemma measurable_prod_g_measurableType : @measurable _ [the measurableType _ of salgebraType C1 * salgebraType C2 : Type] = <<s [set A `*` B | A in C1 & B in C2] >>.
proof: Proof. rewrite measurable_prod_measurableType //; congr (<<s _ >>). rewrite predeqE => X; split=> [[A mA] [B mB] <-{X}|[A C1A] [B C2B] <-{X}]. by exists A; [exact: setTC1|exists B => //; exact: setTC2]. by exists A; [exact: sub_sigma_algebra|exists B => //; 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)