proposition: Lemma nd_sintegral_lim : sintegral mu f = limn (sintegral mu \o g).
proof: Proof. apply/eqP; rewrite eq_le; apply/andP; split. by apply: nd_sintegral_lim_lemma => // x; rewrite -limg. have : nondecreasing_seq (sintegral mu \o g). by move=> m n mn; apply: le_sintegral => // x; exact/nd_g. move=> /ereal_nondecreasing_cvgn/cvg_lim -> //. apply: ub_ereal_sup => _ [n _ <-] /=; apply: le_sintegral => // x. rewrite -limg // (nondecreasing_cvgn_le (nd_g x)) //. by apply/cvg_ex; exists (f x); exact: gf. 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