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.6    apply (simp add: norm_vec_def)
     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