src/HOL/Real_Vector_Spaces.thy
changeset 59741 5b762cd73a8e
parent 59658 0cc388370041
child 59867 58043346ca64
     1.1 --- a/src/HOL/Real_Vector_Spaces.thy	Tue Mar 17 17:45:03 2015 +0000
     1.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Wed Mar 18 14:13:27 2015 +0000
     1.3 @@ -444,7 +444,8 @@
     1.4    then show thesis ..
     1.5  qed
     1.6  
     1.7 -lemma setsum_in_Reals: assumes "\<And>i. i \<in> s \<Longrightarrow> f i \<in> \<real>" shows "setsum f s \<in> \<real>"
     1.8 +lemma setsum_in_Reals [intro,simp]:
     1.9 +  assumes "\<And>i. i \<in> s \<Longrightarrow> f i \<in> \<real>" shows "setsum f s \<in> \<real>"
    1.10  proof (cases "finite s")
    1.11    case True then show ?thesis using assms
    1.12      by (induct s rule: finite_induct) auto
    1.13 @@ -453,7 +454,8 @@
    1.14      by (metis Reals_0 setsum.infinite)
    1.15  qed
    1.16  
    1.17 -lemma setprod_in_Reals: assumes "\<And>i. i \<in> s \<Longrightarrow> f i \<in> \<real>" shows "setprod f s \<in> \<real>"
    1.18 +lemma setprod_in_Reals [intro,simp]: 
    1.19 +  assumes "\<And>i. i \<in> s \<Longrightarrow> f i \<in> \<real>" shows "setprod f s \<in> \<real>"
    1.20  proof (cases "finite s")
    1.21    case True then show ?thesis using assms
    1.22      by (induct s rule: finite_induct) auto