proposition: Lemma integrableS (E D : set T) (f : T -> \bar R) : measurable E -> measurable D -> D `<=` E -> mu.-integrable E f -> mu.-integrable D f.
proof: Proof. move=> mE mD DE /integrableP[mf ifoo]; apply/integrableP; split. exact: measurable_funS mf. apply: le_lt_trans ifoo; apply: subset_integral => //. exact: measurableT_comp. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum ssrint interval finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop ) signed reals ereal topology normedtype sequences real_interval esum measure lebesgue_measure numfun