proposition: Lemma ereal_nonincreasing_cvgn (R : realType) (u_ : (\bar R)^nat) : nonincreasing_seq u_ -> u_ @ \oo --> ereal_inf (u_ @` setT).
proof: Proof. move=> ni_u; rewrite [X in X @ \oo --> _](_ : _ = -%E \o -%E \o u_); last first. by rewrite funeqE => n; rewrite /= oppeK. apply: cvgeN. rewrite [X in _ --> X](_ : _ = ereal_sup (range (-%E \o u_))); last first. congr ereal_sup; rewrite predeqE => x; split=> [[_ [n _ <-]] <-|[n _] <-]; by [exists n | exists (u_ n) => //; exists n]. by apply: ereal_nondecreasing_cvgn; rewrite ereal_nondecreasing_oppn. 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