equal
deleted
inserted
replaced
218 |
218 |
219 lemma norm_cmul_rule_thm: |
219 lemma norm_cmul_rule_thm: |
220 fixes x :: "'a::real_normed_vector" |
220 fixes x :: "'a::real_normed_vector" |
221 shows "b >= norm(x) ==> \<bar>c\<bar> * b >= norm(scaleR c x)" |
221 shows "b >= norm(x) ==> \<bar>c\<bar> * b >= norm(scaleR c x)" |
222 unfolding norm_scaleR |
222 unfolding norm_scaleR |
223 apply (erule mult_mono1) |
223 apply (erule mult_left_mono) |
224 apply simp |
224 apply simp |
225 done |
225 done |
226 |
226 |
227 (* FIXME: Move all these theorems into the ML code using lemma antiquotation *) |
227 (* FIXME: Move all these theorems into the ML code using lemma antiquotation *) |
228 lemma norm_add_rule_thm: |
228 lemma norm_add_rule_thm: |