proposition: Lemma nlim_sup (u : nat -> R) l : (forall n m, (n <= m)%N -> u n <= u m) -> ncvg u l%:E -> sup [set r | exists n, r = u n] = l.
proof: Proof. move=> mn_u cv_ul; set S := (X in sup X); suff: ncvg u (sup S)%:E. by move/nlimE; move/nlimE: cv_ul => -> [->]. elim/nbh_finW=> /= e gt0_e; have sS: has_sup S. split; first exists (u 0%N). by exists 0%N. exists l; apply/ubP => _ [n ->]. by rewrite -lee_fin; apply/ncvg_homo_le. have /sup_adherent := sS => /(_ _ gt0_e) [r] [N ->] lt_uN. exists N => n le_Nn; rewrite !inE distrC ger0_norm ?subr_ge0. by move/ubP : (sup_upper_bound sS) => -> //; exists n. by rewrite ltrBlDr -ltrBlDl (lt_le_trans lt_uN) ?mn_u. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.bigenough.bigenough mathcomp.classical(boolp classical_sets functions) mathcomp.classical(mathcomp_extra) xfinmap ereal reals discrete topology