# HG changeset patch
# User nipkow
# Date 1512658130 -3600
# Node ID 9e5b05d54f9dc28c6c3b2da54067e9f429ee8b8c
# Parent  c7def8f836d09be51fdf5e705f9febaaa8a3abe9
canonical name

diff -r c7def8f836d0 -r 9e5b05d54f9d src/HOL/Analysis/Cartesian_Euclidean_Space.thy
--- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Thu Dec 07 11:14:32 2017 +0100
+++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Thu Dec 07 15:48:50 2017 +0100
@@ -290,7 +290,7 @@
 
 lemma component_le_norm_cart: "\<bar>x$i\<bar> <= norm x"
   apply (simp add: norm_vec_def)
-  apply (rule member_le_setL2, simp_all)
+  apply (rule member_le_L2_set, simp_all)
   done
 
 lemma norm_bound_component_le_cart: "norm x <= e ==> \<bar>x$i\<bar> <= e"
@@ -300,7 +300,7 @@
   by (metis component_le_norm_cart le_less_trans)
 
 lemma norm_le_l1_cart: "norm x <= sum(\<lambda>i. \<bar>x$i\<bar>) UNIV"
-  by (simp add: norm_vec_def setL2_le_sum)
+  by (simp add: norm_vec_def L2_set_le_sum)
 
 lemma scalar_mult_eq_scaleR: "c *s x = c *\<^sub>R x"
   unfolding scaleR_vec_def vector_scalar_mult_def by simp
@@ -984,7 +984,7 @@
     { fix n
       assume n: "\<forall>i. dist (f (r n) $ i) (l $ i) < e / (real_of_nat (card ?d))"
       have "dist (f (r n)) l \<le> (\<Sum>i\<in>?d. dist (f (r n) $ i) (l $ i))"
-        unfolding dist_vec_def using zero_le_dist by (rule setL2_le_sum)
+        unfolding dist_vec_def using zero_le_dist by (rule L2_set_le_sum)
       also have "\<dots> < (\<Sum>i\<in>?d. e / (real_of_nat (card ?d)))"
         by (rule sum_strict_mono) (simp_all add: n)
       finally have "dist (f (r n)) l < e" by simp
diff -r c7def8f836d0 -r 9e5b05d54f9d src/HOL/Analysis/Connected.thy
--- a/src/HOL/Analysis/Connected.thy	Thu Dec 07 11:14:32 2017 +0100
+++ b/src/HOL/Analysis/Connected.thy	Thu Dec 07 15:48:50 2017 +0100
@@ -2854,7 +2854,7 @@
 lemma diameter_cbox:
   fixes a b::"'a::euclidean_space"
   shows "(\<forall>i \<in> Basis. a \<bullet> i \<le> b \<bullet> i) \<Longrightarrow> diameter (cbox a b) = dist a b"
-  by (force simp: diameter_def intro!: cSup_eq_maximum setL2_mono
+  by (force simp: diameter_def intro!: cSup_eq_maximum L2_set_mono
      simp: euclidean_dist_l2[where 'a='a] cbox_def dist_norm)
 
 subsection \<open>Separation between points and sets\<close>
@@ -5038,7 +5038,7 @@
 
 text\<open>But is the premise really necessary? Need to generalise @{thm euclidean_dist_l2}\<close>
 lemma Euclidean_dist_upper: "i \<in> Basis \<Longrightarrow> dist (x \<bullet> i) (y \<bullet> i) \<le> dist x y"
-  by (metis (no_types) member_le_setL2 euclidean_dist_l2 finite_Basis)
+  by (metis (no_types) member_le_L2_set euclidean_dist_l2 finite_Basis)
 
 text\<open>But is the premise @{term \<open>i \<in> Basis\<close>} really necessary?\<close>
 lemma open_preimage_inner:
@@ -5087,17 +5087,17 @@
   proof clarify
     fix e::real
     assume "0 < e"
-    have *: "setL2 (\<lambda>i. dist (f x \<bullet> i) (l \<bullet> i)) Basis < e"
+    have *: "L2_set (\<lambda>i. dist (f x \<bullet> i) (l \<bullet> i)) Basis < e"
              if "\<forall>i\<in>Basis. dist (f x \<bullet> i) (l \<bullet> i) < e / real DIM('b)" for x
     proof -
-      have "setL2 (\<lambda>i. dist (f x \<bullet> i) (l \<bullet> i)) Basis \<le> sum (\<lambda>i. dist (f x \<bullet> i) (l \<bullet> i)) Basis"
-        by (simp add: setL2_le_sum)
+      have "L2_set (\<lambda>i. dist (f x \<bullet> i) (l \<bullet> i)) Basis \<le> sum (\<lambda>i. dist (f x \<bullet> i) (l \<bullet> i)) Basis"
+        by (simp add: L2_set_le_sum)
       also have "... < DIM('b) * (e / real DIM('b))"
         apply (rule sum_bounded_above_strict)
         using that by auto
       also have "... = e"
         by (simp add: field_simps)
-      finally show "setL2 (\<lambda>i. dist (f x \<bullet> i) (l \<bullet> i)) Basis < e" .
+      finally show "L2_set (\<lambda>i. dist (f x \<bullet> i) (l \<bullet> i)) Basis < e" .
     qed
     have "\<forall>\<^sub>F x in F. \<forall>i\<in>Basis. dist (f x \<bullet> i) (l \<bullet> i) < e / DIM('b)"
       apply (rule R')
@@ -5516,7 +5516,7 @@
     by (auto intro!: sum_mono simp: clamp_def dist_real_def abs_le_square_iff[symmetric])
   then show ?thesis
     by (auto intro: real_sqrt_le_mono
-      simp: euclidean_dist_l2[where y=x] euclidean_dist_l2[where y="clamp a b x"] setL2_def)
+      simp: euclidean_dist_l2[where y=x] euclidean_dist_l2[where y="clamp a b x"] L2_set_def)
 qed (auto simp: clamp_def)
 
 lemma clamp_continuous_at:
diff -r c7def8f836d0 -r 9e5b05d54f9d src/HOL/Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Thu Dec 07 11:14:32 2017 +0100
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Thu Dec 07 15:48:50 2017 +0100
@@ -7262,7 +7262,7 @@
       unfolding 2
       apply clarsimp
       apply (subst euclidean_dist_l2)
-      apply (rule order_trans [OF setL2_le_sum])
+      apply (rule order_trans [OF L2_set_le_sum])
       apply (rule zero_le_dist)
       unfolding e'
       apply (rule sum_mono)
diff -r c7def8f836d0 -r 9e5b05d54f9d src/HOL/Analysis/Finite_Cartesian_Product.thy
--- a/src/HOL/Analysis/Finite_Cartesian_Product.thy	Thu Dec 07 11:14:32 2017 +0100
+++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy	Thu Dec 07 15:48:50 2017 +0100
@@ -342,7 +342,7 @@
 begin
 
 definition
-  "dist x y = setL2 (\<lambda>i. dist (x$i) (y$i)) UNIV"
+  "dist x y = L2_set (\<lambda>i. dist (x$i) (y$i)) UNIV"
 
 instance ..
 end
@@ -364,19 +364,19 @@
 begin
 
 lemma dist_vec_nth_le: "dist (x $ i) (y $ i) \<le> dist x y"
-  unfolding dist_vec_def by (rule member_le_setL2) simp_all
+  unfolding dist_vec_def by (rule member_le_L2_set) simp_all
 
 instance proof
   fix x y :: "'a ^ 'b"
   show "dist x y = 0 \<longleftrightarrow> x = y"
     unfolding dist_vec_def
-    by (simp add: setL2_eq_0_iff vec_eq_iff)
+    by (simp add: L2_set_eq_0_iff vec_eq_iff)
 next
   fix x y z :: "'a ^ 'b"
   show "dist x y \<le> dist x z + dist y z"
     unfolding dist_vec_def
-    apply (rule order_trans [OF _ setL2_triangle_ineq])
-    apply (simp add: setL2_mono dist_triangle2)
+    apply (rule order_trans [OF _ L2_set_triangle_ineq])
+    apply (simp add: L2_set_mono dist_triangle2)
     done
 next
   fix S :: "('a ^ 'b) set"
@@ -407,13 +407,13 @@
       define r where [abs_def]: "r i = e / sqrt (of_nat CARD('b))" for i :: 'b
       from \<open>0 < e\<close> have r: "\<forall>i. 0 < r i"
         unfolding r_def by simp_all
-      from \<open>0 < e\<close> have e: "e = setL2 r UNIV"
-        unfolding r_def by (simp add: setL2_constant)
+      from \<open>0 < e\<close> have e: "e = L2_set r UNIV"
+        unfolding r_def by (simp add: L2_set_constant)
       define A where "A i = {y. dist (x $ i) y < r i}" for i
       have "\<forall>i. open (A i) \<and> x $ i \<in> A i"
         unfolding A_def by (simp add: open_ball r)
       moreover have "\<forall>y. (\<forall>i. y $ i \<in> A i) \<longrightarrow> y \<in> S"
-        by (simp add: A_def S dist_vec_def e setL2_strict_mono dist_commute)
+        by (simp add: A_def S dist_vec_def e L2_set_strict_mono dist_commute)
       ultimately show "\<exists>A. (\<forall>i. open (A i) \<and> x $ i \<in> A i) \<and>
         (\<forall>y. (\<forall>i. y $ i \<in> A i) \<longrightarrow> y \<in> S)" by metis
     qed
@@ -447,10 +447,10 @@
   {
     fix m n :: nat
     assume "M \<le> m" "M \<le> n"
-    have "dist (X m) (X n) = setL2 (\<lambda>i. dist (X m $ i) (X n $ i)) UNIV"
+    have "dist (X m) (X n) = L2_set (\<lambda>i. dist (X m $ i) (X n $ i)) UNIV"
       unfolding dist_vec_def ..
     also have "\<dots> \<le> sum (\<lambda>i. dist (X m $ i) (X n $ i)) UNIV"
-      by (rule setL2_le_sum [OF zero_le_dist])
+      by (rule L2_set_le_sum [OF zero_le_dist])
     also have "\<dots> < sum (\<lambda>i::'n. ?s) UNIV"
       by (rule sum_strict_mono, simp_all add: M \<open>M \<le> m\<close> \<open>M \<le> n\<close>)
     also have "\<dots> = r"
@@ -480,7 +480,7 @@
 instantiation vec :: (real_normed_vector, finite) real_normed_vector
 begin
 
-definition "norm x = setL2 (\<lambda>i. norm (x$i)) UNIV"
+definition "norm x = L2_set (\<lambda>i. norm (x$i)) UNIV"
 
 definition "sgn (x::'a^'b) = scaleR (inverse (norm x)) x"
 
@@ -488,15 +488,15 @@
   fix a :: real and x y :: "'a ^ 'b"
   show "norm x = 0 \<longleftrightarrow> x = 0"
     unfolding norm_vec_def
-    by (simp add: setL2_eq_0_iff vec_eq_iff)
+    by (simp add: L2_set_eq_0_iff vec_eq_iff)
   show "norm (x + y) \<le> norm x + norm y"
     unfolding norm_vec_def
-    apply (rule order_trans [OF _ setL2_triangle_ineq])
-    apply (simp add: setL2_mono norm_triangle_ineq)
+    apply (rule order_trans [OF _ L2_set_triangle_ineq])
+    apply (simp add: L2_set_mono norm_triangle_ineq)
     done
   show "norm (scaleR a x) = \<bar>a\<bar> * norm x"
     unfolding norm_vec_def
-    by (simp add: setL2_right_distrib)
+    by (simp add: L2_set_right_distrib)
   show "sgn x = scaleR (inverse (norm x)) x"
     by (rule sgn_vec_def)
   show "dist x y = norm (x - y)"
@@ -508,7 +508,7 @@
 
 lemma norm_nth_le: "norm (x $ i) \<le> norm x"
 unfolding norm_vec_def
-by (rule member_le_setL2) simp_all
+by (rule member_le_L2_set) simp_all
 
 lemma bounded_linear_vec_nth: "bounded_linear (\<lambda>x. x $ i)"
 apply standard
@@ -545,7 +545,7 @@
     unfolding inner_vec_def
     by (simp add: vec_eq_iff sum_nonneg_eq_0_iff)
   show "norm x = sqrt (inner x x)"
-    unfolding inner_vec_def norm_vec_def setL2_def
+    unfolding inner_vec_def norm_vec_def L2_set_def
     by (simp add: power2_norm_eq_inner)
 qed
 
diff -r c7def8f836d0 -r 9e5b05d54f9d src/HOL/Analysis/L2_Norm.thy
--- a/src/HOL/Analysis/L2_Norm.thy	Thu Dec 07 11:14:32 2017 +0100
+++ b/src/HOL/Analysis/L2_Norm.thy	Thu Dec 07 15:48:50 2017 +0100
@@ -8,74 +8,73 @@
 imports Complex_Main
 begin
 
-definition
-  "setL2 f A = sqrt (\<Sum>i\<in>A. (f i)\<^sup>2)"
+definition "L2_set f A = sqrt (\<Sum>i\<in>A. (f i)\<^sup>2)"
 
-lemma setL2_cong:
-  "\<lbrakk>A = B; \<And>x. x \<in> B \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> setL2 f A = setL2 g B"
-  unfolding setL2_def by simp
+lemma L2_set_cong:
+  "\<lbrakk>A = B; \<And>x. x \<in> B \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> L2_set f A = L2_set g B"
+  unfolding L2_set_def by simp
 
-lemma strong_setL2_cong:
-  "\<lbrakk>A = B; \<And>x. x \<in> B =simp=> f x = g x\<rbrakk> \<Longrightarrow> setL2 f A = setL2 g B"
-  unfolding setL2_def simp_implies_def by simp
+lemma strong_L2_set_cong:
+  "\<lbrakk>A = B; \<And>x. x \<in> B =simp=> f x = g x\<rbrakk> \<Longrightarrow> L2_set f A = L2_set g B"
+  unfolding L2_set_def simp_implies_def by simp
 
-lemma setL2_infinite [simp]: "\<not> finite A \<Longrightarrow> setL2 f A = 0"
-  unfolding setL2_def by simp
+lemma L2_set_infinite [simp]: "\<not> finite A \<Longrightarrow> L2_set f A = 0"
+  unfolding L2_set_def by simp
+
+lemma L2_set_empty [simp]: "L2_set f {} = 0"
+  unfolding L2_set_def by simp
 
-lemma setL2_empty [simp]: "setL2 f {} = 0"
-  unfolding setL2_def by simp
+lemma L2_set_insert [simp]:
+  "\<lbrakk>finite F; a \<notin> F\<rbrakk> \<Longrightarrow>
+    L2_set f (insert a F) = sqrt ((f a)\<^sup>2 + (L2_set f F)\<^sup>2)"
+  unfolding L2_set_def by (simp add: sum_nonneg)
 
-lemma setL2_insert [simp]:
-  "\<lbrakk>finite F; a \<notin> F\<rbrakk> \<Longrightarrow>
-    setL2 f (insert a F) = sqrt ((f a)\<^sup>2 + (setL2 f F)\<^sup>2)"
-  unfolding setL2_def by (simp add: sum_nonneg)
+lemma L2_set_nonneg [simp]: "0 \<le> L2_set f A"
+  unfolding L2_set_def by (simp add: sum_nonneg)
 
-lemma setL2_nonneg [simp]: "0 \<le> setL2 f A"
-  unfolding setL2_def by (simp add: sum_nonneg)
+lemma L2_set_0': "\<forall>a\<in>A. f a = 0 \<Longrightarrow> L2_set f A = 0"
+  unfolding L2_set_def by simp
 
-lemma setL2_0': "\<forall>a\<in>A. f a = 0 \<Longrightarrow> setL2 f A = 0"
-  unfolding setL2_def by simp
+lemma L2_set_constant: "L2_set (\<lambda>x. y) A = sqrt (of_nat (card A)) * \<bar>y\<bar>"
+  unfolding L2_set_def by (simp add: real_sqrt_mult)
 
-lemma setL2_constant: "setL2 (\<lambda>x. y) A = sqrt (of_nat (card A)) * \<bar>y\<bar>"
-  unfolding setL2_def by (simp add: real_sqrt_mult)
-
-lemma setL2_mono:
+lemma L2_set_mono:
   assumes "\<And>i. i \<in> K \<Longrightarrow> f i \<le> g i"
   assumes "\<And>i. i \<in> K \<Longrightarrow> 0 \<le> f i"
-  shows "setL2 f K \<le> setL2 g K"
-  unfolding setL2_def
+  shows "L2_set f K \<le> L2_set g K"
+  unfolding L2_set_def
   by (simp add: sum_nonneg sum_mono power_mono assms)
 
-lemma setL2_strict_mono:
+lemma L2_set_strict_mono:
   assumes "finite K" and "K \<noteq> {}"
   assumes "\<And>i. i \<in> K \<Longrightarrow> f i < g i"
   assumes "\<And>i. i \<in> K \<Longrightarrow> 0 \<le> f i"
-  shows "setL2 f K < setL2 g K"
-  unfolding setL2_def
+  shows "L2_set f K < L2_set g K"
+  unfolding L2_set_def
   by (simp add: sum_strict_mono power_strict_mono assms)
 
-lemma setL2_right_distrib:
-  "0 \<le> r \<Longrightarrow> r * setL2 f A = setL2 (\<lambda>x. r * f x) A"
-  unfolding setL2_def
+lemma L2_set_right_distrib:
+  "0 \<le> r \<Longrightarrow> r * L2_set f A = L2_set (\<lambda>x. r * f x) A"
+  unfolding L2_set_def
   apply (simp add: power_mult_distrib)
   apply (simp add: sum_distrib_left [symmetric])
   apply (simp add: real_sqrt_mult sum_nonneg)
   done
 
-lemma setL2_left_distrib:
-  "0 \<le> r \<Longrightarrow> setL2 f A * r = setL2 (\<lambda>x. f x * r) A"
-  unfolding setL2_def
+lemma L2_set_left_distrib:
+  "0 \<le> r \<Longrightarrow> L2_set f A * r = L2_set (\<lambda>x. f x * r) A"
+  unfolding L2_set_def
   apply (simp add: power_mult_distrib)
   apply (simp add: sum_distrib_right [symmetric])
   apply (simp add: real_sqrt_mult sum_nonneg)
   done
 
-lemma setL2_eq_0_iff: "finite A \<Longrightarrow> setL2 f A = 0 \<longleftrightarrow> (\<forall>x\<in>A. f x = 0)"
-  unfolding setL2_def
+lemma L2_set_eq_0_iff: "finite A \<Longrightarrow> L2_set f A = 0 \<longleftrightarrow> (\<forall>x\<in>A. f x = 0)"
+  unfolding L2_set_def
   by (simp add: sum_nonneg sum_nonneg_eq_0_iff)
 
-lemma setL2_triangle_ineq:
-  shows "setL2 (\<lambda>i. f i + g i) A \<le> setL2 f A + setL2 g A"
+lemma L2_set_triangle_ineq:
+  shows "L2_set (\<lambda>i. f i + g i) A \<le> L2_set f A + L2_set g A"
 proof (cases "finite A")
   case False
   thus ?thesis by simp
@@ -87,12 +86,12 @@
     show ?case by simp
   next
     case (insert x F)
-    hence "sqrt ((f x + g x)\<^sup>2 + (setL2 (\<lambda>i. f i + g i) F)\<^sup>2) \<le>
-           sqrt ((f x + g x)\<^sup>2 + (setL2 f F + setL2 g F)\<^sup>2)"
+    hence "sqrt ((f x + g x)\<^sup>2 + (L2_set (\<lambda>i. f i + g i) F)\<^sup>2) \<le>
+           sqrt ((f x + g x)\<^sup>2 + (L2_set f F + L2_set g F)\<^sup>2)"
       by (intro real_sqrt_le_mono add_left_mono power_mono insert
-                setL2_nonneg add_increasing zero_le_power2)
+                L2_set_nonneg add_increasing zero_le_power2)
     also have
-      "\<dots> \<le> sqrt ((f x)\<^sup>2 + (setL2 f F)\<^sup>2) + sqrt ((g x)\<^sup>2 + (setL2 g F)\<^sup>2)"
+      "\<dots> \<le> sqrt ((f x)\<^sup>2 + (L2_set f F)\<^sup>2) + sqrt ((g x)\<^sup>2 + (L2_set g F)\<^sup>2)"
       by (rule real_sqrt_sum_squares_triangle_ineq)
     finally show ?case
       using insert by simp
@@ -106,8 +105,8 @@
   apply simp
   done
 
-lemma setL2_le_sum [rule_format]:
-  "(\<forall>i\<in>A. 0 \<le> f i) \<longrightarrow> setL2 f A \<le> sum f A"
+lemma L2_set_le_sum [rule_format]:
+  "(\<forall>i\<in>A. 0 \<le> f i) \<longrightarrow> L2_set f A \<le> sum f A"
   apply (cases "finite A")
   apply (induct set: finite)
   apply simp
@@ -124,7 +123,7 @@
   apply simp
   done
 
-lemma setL2_le_sum_abs: "setL2 f A \<le> (\<Sum>i\<in>A. \<bar>f i\<bar>)"
+lemma L2_set_le_sum_abs: "L2_set f A \<le> (\<Sum>i\<in>A. \<bar>f i\<bar>)"
   apply (cases "finite A")
   apply (induct set: finite)
   apply simp
@@ -134,7 +133,7 @@
   apply simp
   done
 
-lemma setL2_mult_ineq_lemma:
+lemma L2_set_mult_ineq_lemma:
   fixes a b c d :: real
   shows "2 * (a * c) * (b * d) \<le> a\<^sup>2 * d\<^sup>2 + b\<^sup>2 * c\<^sup>2"
 proof -
@@ -147,7 +146,7 @@
     by simp
 qed
 
-lemma setL2_mult_ineq: "(\<Sum>i\<in>A. \<bar>f i\<bar> * \<bar>g i\<bar>) \<le> setL2 f A * setL2 g A"
+lemma L2_set_mult_ineq: "(\<Sum>i\<in>A. \<bar>f i\<bar> * \<bar>g i\<bar>) \<le> L2_set f A * L2_set g A"
   apply (cases "finite A")
   apply (induct set: finite)
   apply simp
@@ -160,12 +159,12 @@
   apply (simp add: power_mult_distrib)
   apply (simp add: distrib_left distrib_right)
   apply (rule ord_le_eq_trans)
-  apply (rule setL2_mult_ineq_lemma)
+  apply (rule L2_set_mult_ineq_lemma)
   apply simp_all
   done
 
-lemma member_le_setL2: "\<lbrakk>finite A; i \<in> A\<rbrakk> \<Longrightarrow> f i \<le> setL2 f A"
-  unfolding setL2_def
+lemma member_le_L2_set: "\<lbrakk>finite A; i \<in> A\<rbrakk> \<Longrightarrow> f i \<le> L2_set f A"
+  unfolding L2_set_def
   by (auto intro!: member_le_sum real_le_rsqrt)
 
 end
diff -r c7def8f836d0 -r 9e5b05d54f9d src/HOL/Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Thu Dec 07 11:14:32 2017 +0100
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Thu Dec 07 15:48:50 2017 +0100
@@ -1249,8 +1249,8 @@
 
 lemma euclidean_dist_l2:
   fixes x y :: "'a :: euclidean_space"
-  shows "dist x y = setL2 (\<lambda>i. dist (x \<bullet> i) (y \<bullet> i)) Basis"
-  unfolding dist_norm norm_eq_sqrt_inner setL2_def
+  shows "dist x y = L2_set (\<lambda>i. dist (x \<bullet> i) (y \<bullet> i)) Basis"
+  unfolding dist_norm norm_eq_sqrt_inner L2_set_def
   by (subst euclidean_inner) (simp add: power2_eq_square inner_diff_left)
 
 lemma eventually_nhds_ball: "d > 0 \<Longrightarrow> eventually (\<lambda>x. x \<in> ball z d) (nhds z)"
@@ -1358,7 +1358,7 @@
     fix y :: 'a
     assume *: "y \<in> box ?a ?b"
     have "dist x y = sqrt (\<Sum>i\<in>Basis. (dist (x \<bullet> i) (y \<bullet> i))\<^sup>2)"
-      unfolding setL2_def[symmetric] by (rule euclidean_dist_l2)
+      unfolding L2_set_def[symmetric] by (rule euclidean_dist_l2)
     also have "\<dots> < sqrt (\<Sum>(i::'a)\<in>Basis. e^2 / real (DIM('a)))"
     proof (rule real_sqrt_less_mono, rule sum_strict_mono)
       fix i :: "'a"
@@ -1460,7 +1460,7 @@
     fix y :: 'a
     assume *: "y \<in> cbox ?a ?b"
     have "dist x y = sqrt (\<Sum>i\<in>Basis. (dist (x \<bullet> i) (y \<bullet> i))\<^sup>2)"
-      unfolding setL2_def[symmetric] by (rule euclidean_dist_l2)
+      unfolding L2_set_def[symmetric] by (rule euclidean_dist_l2)
     also have "\<dots> < sqrt (\<Sum>(i::'a)\<in>Basis. e^2 / real (DIM('a)))"
     proof (rule real_sqrt_less_mono, rule sum_strict_mono)
       fix i :: "'a"
@@ -4579,7 +4579,7 @@
       have "dist (f (r n)) l \<le> (\<Sum>i\<in>Basis. dist (f (r n) \<bullet> i) (l \<bullet> i))"
         apply (subst euclidean_dist_l2)
         using zero_le_dist
-        apply (rule setL2_le_sum)
+        apply (rule L2_set_le_sum)
         done
       also have "\<dots> < (\<Sum>i\<in>(Basis::'a set). e / (real_of_nat DIM('a)))"
         apply (rule sum_strict_mono)