# HG changeset patch
# User huffman
# Date 1158366958 -7200
# Node ID ba543692bfa1aaa383c25e0f6ed03da4dcdd9166
# Parent  5a925ad63f4d1549be4e3a943b2144cc50de31df
add theorem norm_diff_triangle_ineq

diff -r 5a925ad63f4d -r ba543692bfa1 src/HOL/Real/RealVector.thy
--- a/src/HOL/Real/RealVector.thy	Sat Sep 16 02:32:48 2006 +0200
+++ b/src/HOL/Real/RealVector.thy	Sat Sep 16 02:35:58 2006 +0200
@@ -157,6 +157,17 @@
     by simp
 qed
 
+lemma norm_diff_triangle_ineq:
+  fixes a b c d :: "'a::real_normed_vector"
+  shows "norm ((a + b) - (c + d)) \<le> norm (a - c) + norm (b - d)"
+proof -
+  have "norm ((a + b) - (c + d)) = norm ((a - c) + (b - d))"
+    by (simp add: diff_minus add_ac)
+  also have "\<dots> \<le> norm (a - c) + norm (b - d)"
+    by (rule norm_triangle_ineq)
+  finally show ?thesis .
+qed
+
 lemma nonzero_norm_inverse:
   fixes a :: "'a::real_normed_div_algebra"
   shows "a \<noteq> 0 \<Longrightarrow> norm (inverse a) = inverse (norm a)"