proposition: Lemma esum_set_image [R : realType] [T : choiceType] [a : T -> \bar R] [e : nat -> T] [P : set nat] : (forall n : nat, P n -> 0 <= a (e n)) -> set_inj P e -> \esum_(i in [set e x | x in P]) a i = \sum_(i <oo | i \in P) a (e i).
proof: Proof. move=> a0 einj; rewrite esum_image// nneseries_esum ?set_mem_set//. by move=> n; rewrite inE => /a0. 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