src/HOL/Analysis/Connected.thy
changeset 67155 9e5b05d54f9d
parent 66953 826a5fd4d36c
child 67237 1fe0ec14a90a
     1.1 --- a/src/HOL/Analysis/Connected.thy	Mon Oct 30 19:29:06 2017 +0000
     1.2 +++ b/src/HOL/Analysis/Connected.thy	Thu Dec 07 15:48:50 2017 +0100
     1.3 @@ -2854,7 +2854,7 @@
     1.4  lemma diameter_cbox:
     1.5    fixes a b::"'a::euclidean_space"
     1.6    shows "(\<forall>i \<in> Basis. a \<bullet> i \<le> b \<bullet> i) \<Longrightarrow> diameter (cbox a b) = dist a b"
     1.7 -  by (force simp: diameter_def intro!: cSup_eq_maximum setL2_mono
     1.8 +  by (force simp: diameter_def intro!: cSup_eq_maximum L2_set_mono
     1.9       simp: euclidean_dist_l2[where 'a='a] cbox_def dist_norm)
    1.10  
    1.11  subsection \<open>Separation between points and sets\<close>
    1.12 @@ -5038,7 +5038,7 @@
    1.13  
    1.14  text\<open>But is the premise really necessary? Need to generalise @{thm euclidean_dist_l2}\<close>
    1.15  lemma Euclidean_dist_upper: "i \<in> Basis \<Longrightarrow> dist (x \<bullet> i) (y \<bullet> i) \<le> dist x y"
    1.16 -  by (metis (no_types) member_le_setL2 euclidean_dist_l2 finite_Basis)
    1.17 +  by (metis (no_types) member_le_L2_set euclidean_dist_l2 finite_Basis)
    1.18  
    1.19  text\<open>But is the premise @{term \<open>i \<in> Basis\<close>} really necessary?\<close>
    1.20  lemma open_preimage_inner:
    1.21 @@ -5087,17 +5087,17 @@
    1.22    proof clarify
    1.23      fix e::real
    1.24      assume "0 < e"
    1.25 -    have *: "setL2 (\<lambda>i. dist (f x \<bullet> i) (l \<bullet> i)) Basis < e"
    1.26 +    have *: "L2_set (\<lambda>i. dist (f x \<bullet> i) (l \<bullet> i)) Basis < e"
    1.27               if "\<forall>i\<in>Basis. dist (f x \<bullet> i) (l \<bullet> i) < e / real DIM('b)" for x
    1.28      proof -
    1.29 -      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"
    1.30 -        by (simp add: setL2_le_sum)
    1.31 +      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"
    1.32 +        by (simp add: L2_set_le_sum)
    1.33        also have "... < DIM('b) * (e / real DIM('b))"
    1.34          apply (rule sum_bounded_above_strict)
    1.35          using that by auto
    1.36        also have "... = e"
    1.37          by (simp add: field_simps)
    1.38 -      finally show "setL2 (\<lambda>i. dist (f x \<bullet> i) (l \<bullet> i)) Basis < e" .
    1.39 +      finally show "L2_set (\<lambda>i. dist (f x \<bullet> i) (l \<bullet> i)) Basis < e" .
    1.40      qed
    1.41      have "\<forall>\<^sub>F x in F. \<forall>i\<in>Basis. dist (f x \<bullet> i) (l \<bullet> i) < e / DIM('b)"
    1.42        apply (rule R')
    1.43 @@ -5516,7 +5516,7 @@
    1.44      by (auto intro!: sum_mono simp: clamp_def dist_real_def abs_le_square_iff[symmetric])
    1.45    then show ?thesis
    1.46      by (auto intro: real_sqrt_le_mono
    1.47 -      simp: euclidean_dist_l2[where y=x] euclidean_dist_l2[where y="clamp a b x"] setL2_def)
    1.48 +      simp: euclidean_dist_l2[where y=x] euclidean_dist_l2[where y="clamp a b x"] L2_set_def)
    1.49  qed (auto simp: clamp_def)
    1.50  
    1.51  lemma clamp_continuous_at: