src/HOL/Analysis/Cartesian_Euclidean_Space.thy
 changeset 67155 9e5b05d54f9d parent 66804 3f9bb52082c4 child 67399 eab6ce8368fa
```     1.1 --- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Sun Oct 08 22:28:20 2017 +0200
1.2 +++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Thu Dec 07 15:48:50 2017 +0100
1.3 @@ -290,7 +290,7 @@
1.4
1.5  lemma component_le_norm_cart: "\<bar>x\$i\<bar> <= norm x"
1.7 -  apply (rule member_le_setL2, simp_all)
1.8 +  apply (rule member_le_L2_set, simp_all)
1.9    done
1.10
1.11  lemma norm_bound_component_le_cart: "norm x <= e ==> \<bar>x\$i\<bar> <= e"
1.12 @@ -300,7 +300,7 @@
1.13    by (metis component_le_norm_cart le_less_trans)
1.14
1.15  lemma norm_le_l1_cart: "norm x <= sum(\<lambda>i. \<bar>x\$i\<bar>) UNIV"
1.16 -  by (simp add: norm_vec_def setL2_le_sum)
1.17 +  by (simp add: norm_vec_def L2_set_le_sum)
1.18
1.19  lemma scalar_mult_eq_scaleR: "c *s x = c *\<^sub>R x"
1.20    unfolding scaleR_vec_def vector_scalar_mult_def by simp
1.21 @@ -984,7 +984,7 @@
1.22      { fix n
1.23        assume n: "\<forall>i. dist (f (r n) \$ i) (l \$ i) < e / (real_of_nat (card ?d))"
1.24        have "dist (f (r n)) l \<le> (\<Sum>i\<in>?d. dist (f (r n) \$ i) (l \$ i))"
1.25 -        unfolding dist_vec_def using zero_le_dist by (rule setL2_le_sum)
1.26 +        unfolding dist_vec_def using zero_le_dist by (rule L2_set_le_sum)
1.27        also have "\<dots> < (\<Sum>i\<in>?d. e / (real_of_nat (card ?d)))"
1.28          by (rule sum_strict_mono) (simp_all add: n)
1.29        finally have "dist (f (r n)) l < e" by simp
```