--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Mon Aug 22 15:02:45 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Mon Aug 22 10:19:39 2011 -0700
@@ -1624,10 +1624,6 @@
lemma in_span_basis: "(x::'a::euclidean_space) \<in> span (basis ` {..<DIM('a)})"
unfolding span_basis' ..
-lemma component_le_norm: "\<bar>x$$i\<bar> \<le> norm (x::'a::euclidean_space)"
- unfolding euclidean_component_def
- apply(rule order_trans[OF real_inner_class.Cauchy_Schwarz_ineq2]) by auto
-
lemma norm_bound_component_le: "norm (x::'a::euclidean_space) \<le> e \<Longrightarrow> \<bar>x$$i\<bar> <= e"
by (metis component_le_norm order_trans)