proposition: Lemma measurable_fun_prod (f : T -> T1) (g : T -> T2) : measurable_fun setT f -> measurable_fun setT g -> measurable_fun setT (fun x => (f x, g x)).
proof: Proof. by move=> mf mg; exact/prod_measurable_funP. 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)