proposition: Lemma measurable_fun_kseries (U : set Y) : measurable U -> measurable_fun [set: X] (kseries ^~ U).
proof: Proof. move=> mU. by apply: ge0_emeasurable_fun_sum => // n; 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