proposition: Lemma integral_fune_lt_pinfty (f : T -> \bar R) : mu.-integrable D f -> \int[mu]_(x in D) f x < +oo.
proof: Proof. move=> intf; rewrite (funeposneg f) integralB//; [|exact: integrable_funepos|exact: integrable_funeneg]. rewrite lte_add_pinfty ?integral_funepos_lt_pinfty// lteNl ltNye_eq. by rewrite integrable_neg_fin_num. 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