proposition: Lemma sfinite_kernel : exists s : (R.-fker X ~> Y)^nat, forall x U, measurable U -> k x U = kseries s x U.
proof: Proof. exists (fun n => [the _.-fker _ ~> _ of s n]) => x U mU. by rewrite /s /= /s; by case: cid2 => ? ? ->. 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