proposition: Lemma measurable_max_approxRN_seq n : measurable_fun [set: T] (F_ n).
proof: Proof. elim: n => [|n ih]. rewrite /F_ /max_approxRN_seq. under eq_fun do rewrite big_ord_recr/=; rewrite -/(measurable_fun _ _). under eq_fun do rewrite big_ord0; rewrite -/(measurable_fun _ _). under eq_fun do rewrite maxNye; rewrite -/(measurable_fun _ _). have [+ _] := approxRN_seq_prop 0%N. by rewrite inE /= => -[]// _ _ _; exact: measurable_approxRN_seq. rewrite /F_ /max_approxRN_seq => m. under eq_fun do rewrite big_ord_recr. by apply: measurable_maxe => //; exact: measurable_approxRN_seq. 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