--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Sat Nov 27 17:44:36 2010 -0800
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Sun Nov 28 15:20:51 2010 +0100
@@ -1300,7 +1300,7 @@
shows "finite {abs((x::'a::abs ^'n)$i) |i. i\<in> (UNIV :: 'n set)}"
and "{abs(x$i) |i. i\<in> (UNIV :: 'n::finite set)} \<noteq> {}"
unfolding infnorm_set_image_cart
- by (auto intro: finite_imageI)
+ by auto
lemma component_le_infnorm_cart:
shows "\<bar>x$i\<bar> \<le> infnorm (x::real^'n)"