proposition: Lemma measurable_funU D E (f : T1 -> T2) : measurable D -> measurable E -> measurable_fun (D `|` E) f <-> measurable_fun D f /\ measurable_fun E f.
proof: Proof. move=> mD mE; rewrite -bigcup2E; apply: (iff_trans (measurable_fun_bigcup _ _)). by move=> [//|[//|//=]]. split=> [mf|[Df Dg] [//|[//|/= _ _ Y mY]]]; last by rewrite set0I. by split; [exact: (mf 0%N)|exact: (mf 1%N)]. 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)