proposition: Lemma cvg_sups u l : u @ \oo --> l -> sups u @ \oo --> (l : R^o).
proof: Proof. move=> ul; have [iul <-] := cvg_limn_inf_sup ul. apply/cvg_closeP; split => //; apply: is_cvg_sups. by apply/cvg_ex; eexists; apply: ul. 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