equal
deleted
inserted
replaced
822 proof - |
822 proof - |
823 have "norm (a + - b) \<le> norm a + norm (- b)" |
823 have "norm (a + - b) \<le> norm a + norm (- b)" |
824 by (rule norm_triangle_ineq) |
824 by (rule norm_triangle_ineq) |
825 then show ?thesis by simp |
825 then show ?thesis by simp |
826 qed |
826 qed |
|
827 |
|
828 lemma norm_triangle_le_diff: "norm x + norm y \<le> e \<Longrightarrow> norm (x - y) \<le> e" |
|
829 by (meson norm_triangle_ineq4 order_trans) |
827 |
830 |
828 lemma norm_diff_ineq: "norm a - norm b \<le> norm (a + b)" |
831 lemma norm_diff_ineq: "norm a - norm b \<le> norm (a + b)" |
829 for a b :: "'a::real_normed_vector" |
832 for a b :: "'a::real_normed_vector" |
830 proof - |
833 proof - |
831 have "norm a - norm (- b) \<le> norm (a - - b)" |
834 have "norm a - norm (- b) \<le> norm (a - - b)" |