proposition: Lemma measurable_is_max_approxRN m j : measurable (E m j).
proof: Proof. rewrite is_max_approxRNE; apply: measurableI => /=. rewrite -[X in measurable X]setTI. by apply: emeasurable_fun_eq => //; [exact: measurable_max_approxRN_seq| exact: measurable_approxRN_seq]. rewrite [T in measurable T](_ : _ = \bigcap_(k in `I_j) [set x | g_ k x < g_ j x])//. apply: bigcap_measurable => k _. rewrite -[X in measurable X]setTI; apply: emeasurable_fun_lt => //; 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