--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Wed Feb 17 17:57:37 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Wed Feb 17 18:33:45 2010 +0100
@@ -1042,11 +1042,6 @@
shows "norm x \<le> norm y + norm (x - y)"
using norm_triangle_ineq[of "y" "x - y"] by (simp add: ring_simps)
-lemma norm_triangle_le: "norm(x::real ^ 'n) + norm y <= e ==> norm(x + y) <= e"
- by (metis order_trans norm_triangle_ineq)
-lemma norm_triangle_lt: "norm(x::real ^ 'n) + norm(y) < e ==> norm(x + y) < e"
- by (metis basic_trans_rules(21) norm_triangle_ineq)
-
lemma component_le_norm: "\<bar>x$i\<bar> <= norm x"
apply (simp add: norm_vector_def)
apply (rule member_le_setL2, simp_all)
@@ -1275,6 +1270,22 @@
shows "dist y x1 < e / 2 \<Longrightarrow> dist y x2 < e / 2 \<Longrightarrow> dist x1 x2 < e"
by (rule dist_triangle_half_l, simp_all add: dist_commute)
+
+lemma norm_triangle_half_r:
+ shows "norm (y - x1) < e / 2 \<Longrightarrow> norm (y - x2) < e / 2 \<Longrightarrow> norm (x1 - x2) < e"
+ using dist_triangle_half_r unfolding vector_dist_norm[THEN sym] by auto
+
+lemma norm_triangle_half_l: assumes "norm (x - y) < e / 2" "norm (x' - (y)) < e / 2"
+ shows "norm (x - x') < e"
+ using dist_triangle_half_l[OF assms[unfolded vector_dist_norm[THEN sym]]]
+ unfolding vector_dist_norm[THEN sym] .
+
+lemma norm_triangle_le: "norm(x) + norm y <= e ==> norm(x + y) <= e"
+ by (metis order_trans norm_triangle_ineq)
+
+lemma norm_triangle_lt: "norm(x) + norm(y) < e ==> norm(x + y) < e"
+ by (metis basic_trans_rules(21) norm_triangle_ineq)
+
lemma dist_triangle_add:
fixes x y x' y' :: "'a::real_normed_vector"
shows "dist (x + y) (x' + y') <= dist x x' + dist y y'"