proposition: Lemma measurable_fun_mkcomp_sfinite U : measurable U -> measurable_fun [set: X] ((l \; k) ^~ U).
proof: Proof. move=> mU; apply: (measurable_fun_integral_sfinite_kernel (k ^~ U)) => //. exact/measurable_kernel. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum ssrint interval finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop) reals ereal signed topology normedtype sequences esum measure numfun lebesgue_measure lebesgue_integral