fact: Definition summable := exists (M : R), forall (J : {fset T}), \sum_(x : J) `|f (val x)| <= M.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp) xfinmap ereal reals discrete realseq mathcomp.classical(classical_sets functions mathcomp_extra) topology