1040 lemma norm_triangle_sub: |
1040 lemma norm_triangle_sub: |
1041 fixes x y :: "'a::real_normed_vector" |
1041 fixes x y :: "'a::real_normed_vector" |
1042 shows "norm x \<le> norm y + norm (x - y)" |
1042 shows "norm x \<le> norm y + norm (x - y)" |
1043 using norm_triangle_ineq[of "y" "x - y"] by (simp add: ring_simps) |
1043 using norm_triangle_ineq[of "y" "x - y"] by (simp add: ring_simps) |
1044 |
1044 |
1045 lemma norm_triangle_le: "norm(x::real ^ 'n) + norm y <= e ==> norm(x + y) <= e" |
|
1046 by (metis order_trans norm_triangle_ineq) |
|
1047 lemma norm_triangle_lt: "norm(x::real ^ 'n) + norm(y) < e ==> norm(x + y) < e" |
|
1048 by (metis basic_trans_rules(21) norm_triangle_ineq) |
|
1049 |
|
1050 lemma component_le_norm: "\<bar>x$i\<bar> <= norm x" |
1045 lemma component_le_norm: "\<bar>x$i\<bar> <= norm x" |
1051 apply (simp add: norm_vector_def) |
1046 apply (simp add: norm_vector_def) |
1052 apply (rule member_le_setL2, simp_all) |
1047 apply (rule member_le_setL2, simp_all) |
1053 done |
1048 done |
1054 |
1049 |
1272 |
1267 |
1273 lemma dist_triangle_half_r: |
1268 lemma dist_triangle_half_r: |
1274 fixes x1 x2 y :: "'a::metric_space" |
1269 fixes x1 x2 y :: "'a::metric_space" |
1275 shows "dist y x1 < e / 2 \<Longrightarrow> dist y x2 < e / 2 \<Longrightarrow> dist x1 x2 < e" |
1270 shows "dist y x1 < e / 2 \<Longrightarrow> dist y x2 < e / 2 \<Longrightarrow> dist x1 x2 < e" |
1276 by (rule dist_triangle_half_l, simp_all add: dist_commute) |
1271 by (rule dist_triangle_half_l, simp_all add: dist_commute) |
|
1272 |
|
1273 |
|
1274 lemma norm_triangle_half_r: |
|
1275 shows "norm (y - x1) < e / 2 \<Longrightarrow> norm (y - x2) < e / 2 \<Longrightarrow> norm (x1 - x2) < e" |
|
1276 using dist_triangle_half_r unfolding vector_dist_norm[THEN sym] by auto |
|
1277 |
|
1278 lemma norm_triangle_half_l: assumes "norm (x - y) < e / 2" "norm (x' - (y)) < e / 2" |
|
1279 shows "norm (x - x') < e" |
|
1280 using dist_triangle_half_l[OF assms[unfolded vector_dist_norm[THEN sym]]] |
|
1281 unfolding vector_dist_norm[THEN sym] . |
|
1282 |
|
1283 lemma norm_triangle_le: "norm(x) + norm y <= e ==> norm(x + y) <= e" |
|
1284 by (metis order_trans norm_triangle_ineq) |
|
1285 |
|
1286 lemma norm_triangle_lt: "norm(x) + norm(y) < e ==> norm(x + y) < e" |
|
1287 by (metis basic_trans_rules(21) norm_triangle_ineq) |
1277 |
1288 |
1278 lemma dist_triangle_add: |
1289 lemma dist_triangle_add: |
1279 fixes x y x' y' :: "'a::real_normed_vector" |
1290 fixes x y x' y' :: "'a::real_normed_vector" |
1280 shows "dist (x + y) (x' + y') <= dist x x' + dist y y'" |
1291 shows "dist (x + y) (x' + y') <= dist x x' + dist y y'" |
1281 by norm |
1292 by norm |