proposition: Lemma lim_nnesum (J : Type) (r : seq J) (f : J -> I -> \bar R) (l : J -> \bar R) (P : pred J) : (forall j, P j -> \near F, 0 <= f j F) -> (forall j, P j -> cvg (f j @ F)) -> lim (\sum_(j <- r | P j) f j i @[i --> F]) = \sum_(j <- r | P j) (lim (f j @ F)).
proof: Proof. by move=> ? ?; apply/cvg_lim => //; apply: cvg_nnesum. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrint ssrnum finmap matrix) mathcomp(rat interval zmodp vector fieldext falgebra) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality set_interval Rstruct) ereal reals signed topology prodnormedzmodule