proposition: Lemma integral_measure_sum_nnsfun (D : set T) (mD : measurable D) (f : {nnsfun T >-> R}) : \int[m]_(x in D) (f x)%:E = \sum_(n < N) \int[m_ n]_(x in D) (f x)%:E.
proof: Proof. rewrite integral_mkcond. transitivity (\int[m]_x (proj_nnsfun f mD x)%:E). by apply: eq_integral => t _ /=; rewrite /patch mindicE; case: ifPn => // tD; rewrite ?mulr1 ?mulr0. rewrite integralT_measure_sum; apply: eq_bigr => i _. rewrite [RHS]integral_mkcond; apply: eq_integral => t _. rewrite /= /patch /mindic indicE. by case: (boolP (t \in D)) => tD; rewrite ?mulr1 ?mulr0. 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