proposition: Lemma bigsetU_is_max_approxRN m : \big[setU/set0]_(j < m.+1) E m j = [set: T].
proof: Proof. apply/seteqP; split => // x _; rewrite -bigcup_mkord. pose j := [arg max_(j > @ord0 m) g_ j x]%O. have j0_proof : exists k, (k < m.+1)%N && (g_ k x == g_ j x). by exists j => //; rewrite eqxx andbT. pose j0 := ex_minn j0_proof. have j0m : (j0 < m.+1)%N by rewrite /j0; case: ex_minnP => // ? /andP[]. have j0max k : (k < j0)%N -> g_ k x < g_ j0 x. rewrite /j0; case: ex_minnP => //= j' /andP[j'm j'j] h kj'. rewrite lt_neqAle; apply/andP; split; last first. rewrite (eqP j'j) /j; case: arg_maxP => //= i _. by move/(_ (Ordinal (ltn_trans kj' j'm))); exact. apply/negP => /eqP gkj'. have := h k; rewrite -(eqP j'j) -gkj' eqxx andbT (ltn_trans kj' j'm). by move=> /(_ erefl); rewrite leqNgt kj'. exists j0 => //; split. rewrite /F_ /max_approxRN_seq (bigmax_eq_arg _ ord0)//; last first. by move=> ? _; rewrite leNye. rewrite /j0/=; case: ex_minnP => //= j' /andP[j'm /eqP]. by rewrite /g_ => -> h. by move=> k kj; exact: j0max. 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