# HG changeset patch
# User huffman
# Date 1178663256 -7200
# Node ID 424d6fb675139cbe9b75b6bb422ab31024100225
# Parent  1ec078cca386cdef5bc5b265e6d1bd1c2cd59646
add lemmas norm_add_less, norm_mult_less

diff -r 1ec078cca386 -r 424d6fb67513 src/HOL/Real/RealVector.thy
--- a/src/HOL/Real/RealVector.thy	Tue May 08 23:52:15 2007 +0200
+++ b/src/HOL/Real/RealVector.thy	Wed May 09 00:27:36 2007 +0200
@@ -493,6 +493,18 @@
   shows "\<bar>norm a\<bar> = norm a"
 by (rule abs_of_nonneg [OF norm_ge_zero])
 
+lemma norm_add_less:
+  fixes x y :: "'a::real_normed_vector"
+  shows "\<lbrakk>norm x < r; norm y < s\<rbrakk> \<Longrightarrow> norm (x + y) < r + s"
+by (rule order_le_less_trans [OF norm_triangle_ineq add_strict_mono])
+
+lemma norm_mult_less:
+  fixes x y :: "'a::real_normed_algebra"
+  shows "\<lbrakk>norm x < r; norm y < s\<rbrakk> \<Longrightarrow> norm (x * y) < r * s"
+apply (rule order_le_less_trans [OF norm_mult_ineq])
+apply (simp add: mult_strict_mono')
+done
+
 lemma norm_of_real [simp]:
   "norm (of_real r :: 'a::real_normed_algebra_1) = \<bar>r\<bar>"
 unfolding of_real_def by (simp add: norm_scaleR)