proposition: Lemma measurable_fun_integral_kernel d d' (X : measurableType d) (Y : measurableType d') (R : realType) (l : X -> {measure set Y -> \bar R}) (ml : forall U, measurable U -> measurable_fun [set: X] (l ^~ U)) (k : Y -> \bar R) (k0 : forall z, 0 <= k z) (mk : measurable_fun [set: Y] k) : measurable_fun [set: X] (fun x => \int[l x]_y k y).
proof: Proof. have [k_ [ndk_ k_k]] := approximation measurableT mk (fun x _ => k0 x). by apply: (measurable_fun_preimage_integral ndk_ k_k) => n r; exact/ml. 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