src/HOL/Analysis/Uniform_Limit.thy

   bounded_linear.uniform_limit[OF bounded_linear_divide]
   bounded_linear.uniform_limit[OF bounded_linear_scaleR_right]
   bounded_linear.uniform_limit[OF bounded_linear_mult_left]
   bounded_linear.uniform_limit[OF bounded_linear_mult_right]
   bounded_linear.uniform_limit[OF bounded_linear_scaleR_left]
+
 
 lemmas uniform_limit_uminus[uniform_limit_intros] =
   bounded_linear.uniform_limit[OF bounded_linear_minus[OF bounded_linear_ident]]
 
 lemma uniform_limit_const[uniform_limit_intros]: "uniform_limit S (\<lambda>x. c) c f"

       and sm: "\<And>x. x \<in> cball \<xi> r \<Longrightarrow> (\<lambda>n. a n * (x - \<xi>) ^ n) sums (f x)"
   shows "continuous_on (cball \<xi> r) f"
 apply (rule continuous_on_cong [THEN iffD1, OF refl _ powser_continuous_suminf [OF r]])
 using sm sums_unique by fastforce
 
+lemmas uniform_limit_subset_union = uniform_limit_on_subset[OF uniform_limit_on_Union]
+
 end