src/HOL/Analysis/Topology_Euclidean_Space.thy
 changeset 67155 9e5b05d54f9d parent 66939 04678058308f child 67399 eab6ce8368fa
```     1.1 --- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Mon Oct 30 16:02:59 2017 +0000
1.2 +++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Thu Dec 07 15:48:50 2017 +0100
1.3 @@ -1249,8 +1249,8 @@
1.4
1.5  lemma euclidean_dist_l2:
1.6    fixes x y :: "'a :: euclidean_space"
1.7 -  shows "dist x y = setL2 (\<lambda>i. dist (x \<bullet> i) (y \<bullet> i)) Basis"
1.8 -  unfolding dist_norm norm_eq_sqrt_inner setL2_def
1.9 +  shows "dist x y = L2_set (\<lambda>i. dist (x \<bullet> i) (y \<bullet> i)) Basis"
1.10 +  unfolding dist_norm norm_eq_sqrt_inner L2_set_def
1.11    by (subst euclidean_inner) (simp add: power2_eq_square inner_diff_left)
1.12
1.13  lemma eventually_nhds_ball: "d > 0 \<Longrightarrow> eventually (\<lambda>x. x \<in> ball z d) (nhds z)"
1.14 @@ -1358,7 +1358,7 @@
1.15      fix y :: 'a
1.16      assume *: "y \<in> box ?a ?b"
1.17      have "dist x y = sqrt (\<Sum>i\<in>Basis. (dist (x \<bullet> i) (y \<bullet> i))\<^sup>2)"
1.18 -      unfolding setL2_def[symmetric] by (rule euclidean_dist_l2)
1.19 +      unfolding L2_set_def[symmetric] by (rule euclidean_dist_l2)
1.20      also have "\<dots> < sqrt (\<Sum>(i::'a)\<in>Basis. e^2 / real (DIM('a)))"
1.21      proof (rule real_sqrt_less_mono, rule sum_strict_mono)
1.22        fix i :: "'a"
1.23 @@ -1460,7 +1460,7 @@
1.24      fix y :: 'a
1.25      assume *: "y \<in> cbox ?a ?b"
1.26      have "dist x y = sqrt (\<Sum>i\<in>Basis. (dist (x \<bullet> i) (y \<bullet> i))\<^sup>2)"
1.27 -      unfolding setL2_def[symmetric] by (rule euclidean_dist_l2)
1.28 +      unfolding L2_set_def[symmetric] by (rule euclidean_dist_l2)
1.29      also have "\<dots> < sqrt (\<Sum>(i::'a)\<in>Basis. e^2 / real (DIM('a)))"
1.30      proof (rule real_sqrt_less_mono, rule sum_strict_mono)
1.31        fix i :: "'a"
1.32 @@ -4579,7 +4579,7 @@
1.33        have "dist (f (r n)) l \<le> (\<Sum>i\<in>Basis. dist (f (r n) \<bullet> i) (l \<bullet> i))"
1.34          apply (subst euclidean_dist_l2)
1.35          using zero_le_dist
1.36 -        apply (rule setL2_le_sum)
1.37 +        apply (rule L2_set_le_sum)
1.38          done
1.39        also have "\<dots> < (\<Sum>i\<in>(Basis::'a set). e / (real_of_nat DIM('a)))"
1.40          apply (rule sum_strict_mono)
```