proposition: Lemma measurable_uncurry (T1 T2 : Type) d (T : semiRingOfSetsType d) (G : T1 -> T2 -> set T) (x : T1 * T2) : measurable (G x.1 x.2) <-> measurable (uncurry G x).
proof: Proof. by case: x. 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)