proposition: Lemma measurable_funeM D (f : T -> \bar R) (k : \bar R) : measurable_fun D f -> measurable_fun D (fun x => k * f x)%E.
proof: Proof. by move=> mf; exact/(emeasurable_funM _ mf). 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