proposition: Lemma measurable_fun_xsection_finite_kernel A : A \in measurable -> measurable_fun [set: X] (phi A).
proof: Proof. move: A; suff : measurable `<=` XY by move=> + A; rewrite inE => /[apply] -[]. move=> /= A mA; rewrite /XY/=; split => //; rewrite (_ : phi _ = (fun x => mrestr (k x) measurableT (xsection A x))); last first. by apply/funext => x//=; rewrite /mrestr setIT. apply measurable_prod_subset_xsection_kernel => // x. have [r hr] := measure_uub k; exists r => B mB. by rewrite (le_lt_trans _ (hr x)) // /mrestr /= setIT le_measure// 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