proposition: Lemma limn_esup_le_cvg u l : limn_esup u <= l -> (forall n, l <= u n) -> u @ \oo --> l.
proof: Proof. move=> supul ul; have usupu n : l <= u n <= esups u n. by rewrite ul /=; apply/ereal_sup_ub; exists n => /=. suff : esups u @ \oo --> l. by apply: (@squeeze_cvge _ _ _ _ (cst l)) => //; [exact: nearW|exact: cvg_cst]. apply/cvg_closeP; split; first exact: is_cvg_esups. rewrite closeE//; apply/eqP. rewrite eq_le -[X in X <= _ <= _]limn_esup_lim supul/=. apply: (lime_ge (@is_cvg_esups _ _)); apply: nearW => m. have /le_trans : l <= einfs u m by apply: lb_ereal_inf => _ [p /= pm] <-. by apply; exact: einfs_le_esups. 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