proposition: Lemma measurable_pair1 (x : T1) : measurable_fun [set: T2] (pair x).
proof: Proof. have m1pairx : measurable_fun [set: T2] (fst \o pair x) by exact/measurable_cst. have m2pairx : measurable_fun [set: T2] (snd \o pair x) by exact/measurable_id. 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)