proposition: Lemma nlim_sumR {I : eqType} (u : I -> nat -> R) (r : seq I) : (forall i, i \in r -> iscvg (u i)) -> nlim (fun n => \sum_(i <- r) (u i) n) = (\sum_(i <- r) (fine (nlim (u i)) : R))%:E.
proof: Proof. move=> h; rewrite nlim_sum //; elim: r h => [|i r ih] h. by rewrite !big_nil. rewrite !big_cons; case: (h i); first by rewrite inE eqxx. move=> c /nlimE ->; rewrite ih // => j jr. by apply/h; rewrite inE jr orbT. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.bigenough.bigenough mathcomp.classical(boolp classical_sets functions) mathcomp.classical(mathcomp_extra) xfinmap ereal reals discrete topology