proposition: Lemma measurable_funS E D (f : T1 -> T2) : measurable E -> D `<=` E -> measurable_fun E f -> measurable_fun D f.
proof: Proof. move=> mE DE mf mD; have mC : measurable (E `\` D) by exact: measurableD. move: (mD). have := measurable_funU f mD mC. suff -> : D `|` (E `\` D) = E by move=> [[]] //. by rewrite setDUK. 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)