proposition: Lemma cvgNy_limn_einf_sup u : u @ \oo --> -oo -> (limn_einf u = -oo) * (limn_esup u = -oo).
proof: Proof. move=> uoo; suff: limn_esup u = -oo. by move=> {}uoo; split => //; apply/eqP; rewrite -leeNy_eq -uoo limn_einf_sup. rewrite limn_esup_lim; apply: cvg_lim => //=; apply/cvgeNyPle => M. have /cvgeNyPle/(_ M)[m _ uM] := uoo. near=> n; apply: ub_ereal_sup => _ [k /= nk <-]. by apply: uM => /=; rewrite (leq_trans _ nk)//; near: n; exists m. 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