src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
changeset 57418 6ab1c7cb0b8d
parent 57276 49c51eeaa623
child 57447 87429bdecad5
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Jun 27 22:08:55 2014 +0200
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sat Jun 28 09:16:42 2014 +0200
     1.3 @@ -7173,7 +7173,7 @@
     1.4      then have "(\<Sum>i\<in>d. (x \<bullet> i) *\<^sub>R i) \<in> span d"
     1.5        by (simp add: span_setsum span_clauses)
     1.6      also have "(\<Sum>i\<in>d. (x \<bullet> i) *\<^sub>R i) = (\<Sum>i\<in>Basis. (x \<bullet> i) *\<^sub>R i)"
     1.7 -      by (rule setsum_mono_zero_cong_left [OF finite_Basis d]) (auto simp add: x)
     1.8 +      by (rule setsum.mono_neutral_cong_left [OF finite_Basis d]) (auto simp add: x)
     1.9      finally show "x \<in> span d"
    1.10        unfolding euclidean_representation .
    1.11    qed