proposition: Lemma integrableD f g : mu_int f -> mu_int g -> mu_int (f \+ g).
proof: Proof. move=> /integrableP[mf foo] /integrableP[mg goo]; apply/integrableP; split. exact: emeasurable_funD. apply: (@le_lt_trans _ _ (\int[mu]_(x in D) (`|f x| + `|g x|))). apply: ge0_le_integral => //. - by apply: measurableT_comp => //; exact: emeasurable_funD. - by move=> ? ?; apply: adde_ge0. - by apply: emeasurable_funD; apply: measurableT_comp. - by move=> *; exact: lee_abs_add. by rewrite ge0_integralD //; [exact: lte_add_pinfty| exact: measurableT_comp|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