proposition: Lemma measurable_fun_integral_finite_kernel (l : R.-fker X ~> Y) (k0 : forall z, 0 <= k z) (mk : measurable_fun [set: X * Y] k) : measurable_fun [set: X] (fun x => \int[l x]_y k (x, y)).
proof: Proof. have [k_ [ndk_ k_k]] := approximation measurableT mk (fun x _ => k0 x). apply: (measurable_fun_xsection_integral ndk_ (k_k ^~ Logic.I)) => n r. have [l_ hl_] := measure_uub l. by apply: measurable_fun_xsection_finite_kernel => // /[!inE]. 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