proposition: Lemma prod_measurable_funP (h : T -> T1 * T2) : measurable_fun setT h <-> measurable_fun setT (fst \o h) /\ measurable_fun setT (snd \o h).
proof: Proof. apply: (@iff_trans _ (preimage_classes (fst \o h) (snd \o h) `<=` measurable)). - rewrite preimage_classes_comp; split=> [mf A [C HC <-]|f12]; first exact: mf. by move=> _ A mA; apply: f12; exists A. - split => [h12|[mf1 mf2]]. split => _ A mA; apply: h12; apply: sub_sigma_algebra; by [left; exists A|right; exists A]. apply: smallest_sub; first exact: sigma_algebra_measurable. by rewrite subUset; split=> [|] A [C mC <-]; [exact: mf1|exact: mf2]. 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)