proposition: Lemma measurable_fun_preimage_integral (l : X -> {measure set Y -> \bar R}) : (forall n r, measurable_fun [set: X] (l ^~ (k_ n @^-1` [set r]))) -> measurable_fun [set: X] (fun x => \int[l x]_z k z).
proof: Proof. move=> h; apply: (measurable_fun_xsection_integral (k \o snd) l (fun n => [the {nnsfun _ >-> _} of k_2 n])) => /=. - by rewrite /k_2 => m n mn; apply/lefP => -[x y] /=; exact/lefP/ndk_. - by move=> [x y]; exact: k_k. - move=> n r _ /= B mB. have := h n r measurableT B mB; rewrite !setTI. suff : (l ^~ (k_ n @^-1` [set r])) @^-1` B = (fun x => l x (xsection (k_2 n @^-1` [set r]) x)) @^-1` B by move=> ->. by apply/seteqP; split => x/=; rewrite (comp_preimage _ snd (k_ n)) xsection_preimage_snd. 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