src/HOL/Groups_Big.thy
changeset 61944 5d06ecfdb472
parent 61943 7fba644ed827
child 61952 546958347e05
     1.1 --- a/src/HOL/Groups_Big.thy	Sun Dec 27 22:07:17 2015 +0100
     1.2 +++ b/src/HOL/Groups_Big.thy	Mon Dec 28 01:26:34 2015 +0100
     1.3 @@ -780,7 +780,7 @@
     1.4  
     1.5  lemma setsum_abs[iff]: 
     1.6    fixes f :: "'a => ('b::ordered_ab_group_add_abs)"
     1.7 -  shows "abs (setsum f A) \<le> setsum (%i. abs(f i)) A"
     1.8 +  shows "\<bar>setsum f A\<bar> \<le> setsum (%i. \<bar>f i\<bar>) A"
     1.9  proof (cases "finite A")
    1.10    case True
    1.11    thus ?thesis
    1.12 @@ -796,12 +796,12 @@
    1.13  
    1.14  lemma setsum_abs_ge_zero[iff]:
    1.15    fixes f :: "'a => ('b::ordered_ab_group_add_abs)"
    1.16 -  shows "0 \<le> setsum (%i. abs(f i)) A"
    1.17 +  shows "0 \<le> setsum (%i. \<bar>f i\<bar>) A"
    1.18    by (simp add: setsum_nonneg)
    1.19  
    1.20  lemma abs_setsum_abs[simp]: 
    1.21    fixes f :: "'a => ('b::ordered_ab_group_add_abs)"
    1.22 -  shows "abs (\<Sum>a\<in>A. abs(f a)) = (\<Sum>a\<in>A. abs(f a))"
    1.23 +  shows "\<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar> = (\<Sum>a\<in>A. \<bar>f a\<bar>)"
    1.24  proof (cases "finite A")
    1.25    case True
    1.26    thus ?thesis