diff -r 1eb12389c499 -r a854ca7ca7d9 src/HOL/Analysis/Uniform_Limit.thy
--- a/src/HOL/Analysis/Uniform_Limit.thy	Mon Mar 24 21:24:03 2025 +0000
+++ b/src/HOL/Analysis/Uniform_Limit.thy	Tue Mar 25 21:19:26 2025 +0000
@@ -631,6 +631,22 @@
   qed
 qed
 
+lemma Weierstrass_m_test_general':
+  fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c :: banach"
+  fixes M :: "'a \<Rightarrow> real"
+  assumes norm_le:  "\<And>x y. x \<in> X \<Longrightarrow> y \<in> Y \<Longrightarrow> norm (f x y) \<le> M x"
+  assumes has_sum: "\<And>y. y \<in> Y \<Longrightarrow> ((\<lambda>x. f x y) has_sum S y) X"
+  assumes summable: "M summable_on X"
+  shows "uniform_limit Y (\<lambda>X y. \<Sum>x\<in>X. f x y) S (finite_subsets_at_top X)"
+proof -
+  have "uniform_limit Y (\<lambda>X y. \<Sum>x\<in>X. f x y) (\<lambda>y. \<Sum>\<^sub>\<infinity>x\<in>X. f x y) (finite_subsets_at_top X)"
+    using norm_le summable by (rule Weierstrass_m_test_general)
+  also have "?this \<longleftrightarrow> ?thesis"
+    by (intro uniform_limit_cong refl always_eventually allI ballI)
+       (use has_sum in \<open>auto simp: has_sum_iff\<close>)
+  finally show ?thesis .
+qed
+
 
 subsection\<^marker>\<open>tag unimportant\<close> \<open>Structural introduction rules\<close>