diff -r 6969d0ffc576 -r 7ff71bdcf731 src/HOL/Analysis/Uniform_Limit.thy
--- a/src/HOL/Analysis/Uniform_Limit.thy	Tue Dec 20 22:24:36 2022 +0000
+++ b/src/HOL/Analysis/Uniform_Limit.thy	Wed Dec 21 12:30:48 2022 +0000
@@ -361,6 +361,19 @@
   qed
 qed (metis uniformly_convergent_on_sum_E)
 
+lemma uniform_limit_suminf:
+  fixes f:: "nat \<Rightarrow> 'a::{metric_space, comm_monoid_add} \<Rightarrow> 'a"
+  assumes "uniformly_convergent_on X (\<lambda>n x. \<Sum>k<n. f k x)" 
+  shows "uniform_limit X (\<lambda>n x. \<Sum>k<n. f k x) (\<lambda>x. \<Sum>k. f k x) sequentially"
+proof -
+  obtain S where S: "uniform_limit X (\<lambda>n x. \<Sum>k<n. f k x) S sequentially"
+    using assms uniformly_convergent_on_def by blast
+  then have "(\<Sum>k. f k x) = S x" if "x \<in> X" for x
+    using that sums_iff sums_def by (blast intro: tendsto_uniform_limitI [OF S])
+  with S show ?thesis
+    by (simp cong: uniform_limit_cong')
+qed
+
 text \<open>TODO: remove explicit formulations
   @{thm uniformly_convergent_eq_cauchy uniformly_cauchy_imp_uniformly_convergent}?!\<close>