proposition: Lemma measurable_fun_ltr D f g : measurable_fun D f -> measurable_fun D g -> measurable_fun D (fun x => f x < g x).
proof: Proof. move=> mf mg mD Y mY; have [| | |] := set_bool Y => /eqP ->. - under eq_fun do rewrite -subr_gt0. rewrite preimage_true -preimage_itv_o_infty. by apply: (measurable_funB mg mf) => //; exact: measurable_itv. - under eq_fun do rewrite ltNge -subr_ge0. rewrite preimage_false set_predC setCK -preimage_itv_c_infty. by apply: (measurable_funB mf mg) => //; exact: measurable_itv. - by rewrite preimage_set0 setI0. - by rewrite preimage_setT setIT. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum ssrint interval) mathcomp(finmap fingroup perm rat) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop) reals ereal signed topology numfun normedtype HB(structures) sequences esum measure real_interval realfun exp lebesgue_stieltjes_measure