proposition: Lemma summable_pinfty D f : summable D f -> forall x, D x -> `| f x | < +oo.
proof: Proof. move=> Dfoo x Dx; apply: le_lt_trans Dfoo. rewrite (esumID [set x])// setI1 mem_set// esum_set1// leeDl//. exact: esum_ge0. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop) reals ereal signed topology sequences normedtype numfun