src/HOL/Analysis/Uniform_Limit.thy
changeset 69313 b021008c5397
parent 69260 0a9688695a1b
child 69529 4ab9657b3257
     1.1 --- a/src/HOL/Analysis/Uniform_Limit.thy	Sun Nov 18 09:51:41 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Uniform_Limit.thy	Sun Nov 18 18:07:51 2018 +0000
     1.3 @@ -654,7 +654,7 @@
     1.4  lemma uniform_limit_on_UNION:
     1.5    assumes "finite S"
     1.6    assumes "\<And>s. s \<in> S \<Longrightarrow> uniform_limit (h s) f g F"
     1.7 -  shows "uniform_limit (UNION S h) f g F"
     1.8 +  shows "uniform_limit (\<Union>(h ` S)) f g F"
     1.9    using assms
    1.10    by induct (auto intro: uniform_limit_on_empty uniform_limit_on_Un)
    1.11