proposition: Lemma emeasurable_fun_le f g : measurable_fun D f -> measurable_fun D g -> measurable (D `&` [set x | f x <= g x]).
proof: Proof. move=> mf mg; under eq_set do rewrite -sube_le0. by apply: emeasurable_fun_infty_c => //; exact: emeasurable_funB. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum ssrint interval finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop ) signed reals ereal topology normedtype sequences real_interval esum measure lebesgue_measure numfun