proposition: Lemma summable_sup (S : T -> R) : summable S -> has_sup [set x | exists J : {fset T}, x = \sum_(j : J) `|S (val j)|]%classic.
proof: Proof. case/summableP=> M _ hbd; split. by exists 0, fset0; rewrite big_fset0. by exists M; apply/ubP=> y [J ->]. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp) xfinmap ereal reals discrete realseq mathcomp.classical(classical_sets functions mathcomp_extra) topology