proposition: Lemma emeasurable_fun_eq f g : measurable_fun D f -> measurable_fun D g -> measurable (D `&` [set x | f x = g x]).
proof: Proof. move=> mf mg; rewrite set_eq_le setIIr. by apply: measurableI; apply: emeasurable_fun_le. 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