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)