proposition: Lemma measurable_pair2 (y : T2) : measurable_fun [set: T1] (pair^~ y).
proof: Proof. have m1pairy : measurable_fun [set: T1] (fst \o pair^~y) by exact/measurable_id. have m2pairy : measurable_fun [set: T1] (snd \o pair^~y) by exact/measurable_cst. 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)