proposition: Lemma is_cvg_sintegral d (T : measurableType d) (R : realType) (m : {measure set T -> \bar R}) (f : {nnsfun T >-> R}^nat) : (forall x, nondecreasing_seq (f ^~ x)) -> cvgn (sintegral m \o f).
proof: Proof. move=> nd_f; apply/cvg_ex; eexists; apply/ereal_nondecreasing_cvgn => a b ab. by apply: le_sintegral => // => x; exact/nd_f. 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