src/HOL/Analysis/Linear_Algebra.thy
changeset 66804 3f9bb52082c4
parent 66641 ff2e0115fea4
child 67399 eab6ce8368fa
     1.1 --- a/src/HOL/Analysis/Linear_Algebra.thy	Sun Oct 08 22:28:20 2017 +0200
     1.2 +++ b/src/HOL/Analysis/Linear_Algebra.thy	Sun Oct 08 22:28:20 2017 +0200
     1.3 @@ -1886,7 +1886,7 @@
     1.4    have "(\<Sum>x\<in>P. norm (f x)) \<le> (\<Sum>x\<in>P. \<Sum>b\<in>Basis. \<bar>f x \<bullet> b\<bar>)"
     1.5      by (rule sum_mono) (rule norm_le_l1)
     1.6    also have "(\<Sum>x\<in>P. \<Sum>b\<in>Basis. \<bar>f x \<bullet> b\<bar>) = (\<Sum>b\<in>Basis. \<Sum>x\<in>P. \<bar>f x \<bullet> b\<bar>)"
     1.7 -    by (rule sum.commute)
     1.8 +    by (rule sum.swap)
     1.9    also have "\<dots> \<le> of_nat (card (Basis :: 'n set)) * (2 * e)"
    1.10    proof (rule sum_bounded_above)
    1.11      fix i :: 'n