proposition: Lemma measurable_bounded_integrable (f : T -> R^o) : mu E < +oo -> measurable_fun E f -> [bounded f x | x in E] -> mu.-integrable E (EFin \o f).
proof: Proof. move=> Afin mfA bdA; apply/integrableP; split; first exact/EFin_measurable_fun. have [M [_ mrt]] := bdA; apply: le_lt_trans. apply: (integral_le_bound (`|M| + 1)%:E) => //; first exact: measurableT_comp. by apply: aeW => z Az; rewrite lee_fin mrt// ltr_pwDr// ler_norm. by rewrite lte_mul_pinfty. 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