proposition: Lemma __deprecated__ereal_lim_sum (R : realFieldType) (I : Type) (r : seq I) (f : I -> (\bar R)^nat) (l : I -> \bar R) (P : pred I) : (forall k n, P k -> 0 <= f k n) -> (forall k, P k -> f k @ \oo --> l k) -> (fun n => \sum_(k <- r | P k) f k n) @ \oo --> \sum_(k <- r | P k) l k.
proof: Proof. by move=> f0 ?; apply: cvg_nnesum => // ? ?; apply: nearW => ?; apply: f0. 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