proposition: Lemma is_cvg_int_max_approxRN_seq A : measurable A -> cvg ((fun n => \int[mu]_(x in A) F_ n x) @ \oo).
proof: Proof. move=> mA; apply: ereal_nondecreasing_is_cvgn => a b ab. apply: ge0_le_integral => //. - by move=> ? ?; exact: max_approxRN_seq_ge0. - by apply: measurable_funS (measurable_max_approxRN_seq a). - by move=> ? ?; exact: max_approxRN_seq_ge0. - exact: measurable_funS (measurable_max_approxRN_seq b). - by move=> x _; exact: max_approxRN_seq_nd. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum ssrint interval) mathcomp(finmap fingroup perm rat) mathcomp(mathcomp_extra boolp classical_sets cardinality) mathcomp(functions fsbigop set_interval) HB(structures) reals ereal signed topology numfun normedtype sequences esum measure realfun lebesgue_measure lebesgue_integral