proposition: Lemma cvg_esups u l : u @ \oo --> l -> esups u @ \oo --> l.
proof: Proof. case: l => [l /fine_cvgP[u_fin_num] ul| |]; last 2 first. - exact: cvgy_esups. - exact: cvgNy_esups. have [p _ pu] := u_fin_num; apply/cvg_ballP => _/posnumP[e]. have : EFin \o sups (fine \o u) @ \oo --> l%:E. by apply: continuous_cvg => //; apply: cvg_sups. move=> /cvg_ballP /(_ e%:num (gt0 _))[q _ qsupsu]; near=> n. have -> : esups u n = (EFin \o sups (fine \o u)) n. rewrite /= -ereal_sup_EFin; last 2 first. - apply/has_ubound_sdrop/bounded_fun_has_ubound. by apply/cvg_seq_bounded/cvg_ex; eexists; exact ul. - by eexists; rewrite /sdrop /=; exists n; [|reflexivity]. congr (ereal_sup _). rewrite predeqE => y; split=> [[m /= nm <-{y}]|[r [m /= nm <-{r} <-{y}]]]. have /pu : (p <= m)%N by rewrite (leq_trans _ nm) //; near: n; exists p. by move=> /fineK umE; eexists; [exists m|exact/umE]. have /pu : (p <= m)%N by rewrite (leq_trans _ nm) //; near: n; exists p. by move=> /fineK umE; exists m => //; exact/umE. by apply: qsupsu => /=; near: n; exists q. Unshelve. all: by end_near. Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum matrix) mathcomp(interval rat) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(set_interval) reals ereal signed topology normedtype landau