proposition: Lemma cvg_has_ub u_ : cvgn u_ -> has_ubound [set `|u_ n| | n in setT].
proof: Proof. move=> /cvg_seq_bounded/pinfty_ex_gt0[M M_gt0 /= uM]. by exists M; apply/ubP => x -[n _ <-{x}]; exact: uM. 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