src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
changeset 54775 2d3df8633dad
parent 54489 03ff4d1e6784
child 54780 6fae499e0827
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Dec 16 14:49:18 2013 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Dec 16 17:08:22 2013 +0100
     1.3 @@ -826,7 +826,14 @@
     1.4    unfolding dist_norm norm_eq_sqrt_inner setL2_def
     1.5    by (subst euclidean_inner) (simp add: power2_eq_square inner_diff_left)
     1.6  
     1.7 -definition "box a b = {x. \<forall>i\<in>Basis. a \<bullet> i < x \<bullet> i \<and> x \<bullet> i < b \<bullet> i}"
     1.8 +definition (in euclidean_space) eucl_less (infix "<e" 50)
     1.9 +  where "eucl_less a b \<longleftrightarrow> (\<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i)"
    1.10 +
    1.11 +definition box_eucl_less: "box a b = {x. a <e x \<and> x <e b}"
    1.12 +
    1.13 +lemma box_def: "box a b = {x. \<forall>i\<in>Basis. a \<bullet> i < x \<bullet> i \<and> x \<bullet> i < b \<bullet> i}"
    1.14 +  and in_box_eucl_less: "x \<in> box a b \<longleftrightarrow> a <e x \<and> x <e b"
    1.15 +  by (auto simp: box_eucl_less eucl_less_def)
    1.16  
    1.17  lemma rational_boxes:
    1.18    fixes x :: "'a\<Colon>euclidean_space"
    1.19 @@ -2042,8 +2049,7 @@
    1.20        by auto
    1.21      then have "ball x (infdist x A) \<inter> closure A = {}"
    1.22        apply auto
    1.23 -      apply (metis `0 < infdist x A` `x \<in> closure A` closure_approachable dist_commute
    1.24 -        eucl_less_not_refl euclidean_trans(2) infdist_le)
    1.25 +      apply (metis `x \<in> closure A` closure_approachable dist_commute infdist_le not_less)
    1.26        done
    1.27      then have "x \<notin> closure A"
    1.28        by (metis `0 < infdist x A` centre_in_ball disjoint_iff_not_equal)
    1.29 @@ -5992,25 +5998,25 @@
    1.30  
    1.31  lemma interval:
    1.32    fixes a :: "'a::ordered_euclidean_space"
    1.33 -  shows "{a <..< b} = {x::'a. \<forall>i\<in>Basis. a\<bullet>i < x\<bullet>i \<and> x\<bullet>i < b\<bullet>i}"
    1.34 +  shows "box a b = {x::'a. \<forall>i\<in>Basis. a\<bullet>i < x\<bullet>i \<and> x\<bullet>i < b\<bullet>i}"
    1.35      and "{a .. b} = {x::'a. \<forall>i\<in>Basis. a\<bullet>i \<le> x\<bullet>i \<and> x\<bullet>i \<le> b\<bullet>i}"
    1.36 -  by (auto simp add:set_eq_iff eucl_le[where 'a='a] eucl_less[where 'a='a])
    1.37 +  by (auto simp add:set_eq_iff eucl_le[where 'a='a] box_def)
    1.38  
    1.39  lemma mem_interval:
    1.40    fixes a :: "'a::ordered_euclidean_space"
    1.41 -  shows "x \<in> {a<..<b} \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i < x\<bullet>i \<and> x\<bullet>i < b\<bullet>i)"
    1.42 +  shows "x \<in> box a b \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i < x\<bullet>i \<and> x\<bullet>i < b\<bullet>i)"
    1.43      and "x \<in> {a .. b} \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i \<le> x\<bullet>i \<and> x\<bullet>i \<le> b\<bullet>i)"
    1.44    using interval[of a b]
    1.45 -  by (auto simp add: set_eq_iff eucl_le[where 'a='a] eucl_less[where 'a='a])
    1.46 +  by auto
    1.47  
    1.48  lemma interval_eq_empty:
    1.49    fixes a :: "'a::ordered_euclidean_space"
    1.50 -  shows "({a <..< b} = {} \<longleftrightarrow> (\<exists>i\<in>Basis. b\<bullet>i \<le> a\<bullet>i))" (is ?th1)
    1.51 +  shows "(box a b = {} \<longleftrightarrow> (\<exists>i\<in>Basis. b\<bullet>i \<le> a\<bullet>i))" (is ?th1)
    1.52      and "({a  ..  b} = {} \<longleftrightarrow> (\<exists>i\<in>Basis. b\<bullet>i < a\<bullet>i))" (is ?th2)
    1.53  proof -
    1.54    {
    1.55      fix i x
    1.56 -    assume i: "i\<in>Basis" and as:"b\<bullet>i \<le> a\<bullet>i" and x:"x\<in>{a <..< b}"
    1.57 +    assume i: "i\<in>Basis" and as:"b\<bullet>i \<le> a\<bullet>i" and x:"x\<in>box a b"
    1.58      then have "a \<bullet> i < x \<bullet> i \<and> x \<bullet> i < b \<bullet> i"
    1.59        unfolding mem_interval by auto
    1.60      then have "a\<bullet>i < b\<bullet>i" by auto
    1.61 @@ -6028,7 +6034,7 @@
    1.62        then have "a\<bullet>i < ((1/2) *\<^sub>R (a+b)) \<bullet> i" "((1/2) *\<^sub>R (a+b)) \<bullet> i < b\<bullet>i"
    1.63          by (auto simp: inner_add_left)
    1.64      }
    1.65 -    then have "{a <..< b} \<noteq> {}"
    1.66 +    then have "box a b \<noteq> {}"
    1.67        using mem_interval(1)[of "?x" a b] by auto
    1.68    }
    1.69    ultimately show ?th1 by blast
    1.70 @@ -6062,37 +6068,37 @@
    1.71  lemma interval_ne_empty:
    1.72    fixes a :: "'a::ordered_euclidean_space"
    1.73    shows "{a  ..  b} \<noteq> {} \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i)"
    1.74 -  and "{a <..< b} \<noteq> {} \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i)"
    1.75 +  and "box a b \<noteq> {} \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i)"
    1.76    unfolding interval_eq_empty[of a b] by fastforce+
    1.77  
    1.78  lemma interval_sing:
    1.79    fixes a :: "'a::ordered_euclidean_space"
    1.80    shows "{a .. a} = {a}"
    1.81 -    and "{a<..<a} = {}"
    1.82 +    and "box a a = {}"
    1.83    unfolding set_eq_iff mem_interval eq_iff [symmetric]
    1.84    by (auto intro: euclidean_eqI simp: ex_in_conv)
    1.85  
    1.86  lemma subset_interval_imp:
    1.87    fixes a :: "'a::ordered_euclidean_space"
    1.88    shows "(\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i) \<Longrightarrow> {c .. d} \<subseteq> {a .. b}"
    1.89 -    and "(\<forall>i\<in>Basis. a\<bullet>i < c\<bullet>i \<and> d\<bullet>i < b\<bullet>i) \<Longrightarrow> {c .. d} \<subseteq> {a<..<b}"
    1.90 -    and "(\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i) \<Longrightarrow> {c<..<d} \<subseteq> {a .. b}"
    1.91 -    and "(\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i) \<Longrightarrow> {c<..<d} \<subseteq> {a<..<b}"
    1.92 +    and "(\<forall>i\<in>Basis. a\<bullet>i < c\<bullet>i \<and> d\<bullet>i < b\<bullet>i) \<Longrightarrow> {c .. d} \<subseteq> box a b"
    1.93 +    and "(\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i) \<Longrightarrow> box c d \<subseteq> {a .. b}"
    1.94 +    and "(\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i) \<Longrightarrow> box c d \<subseteq> box a b"
    1.95    unfolding subset_eq[unfolded Ball_def] unfolding mem_interval
    1.96    by (best intro: order_trans less_le_trans le_less_trans less_imp_le)+
    1.97  
    1.98  lemma interval_open_subset_closed:
    1.99    fixes a :: "'a::ordered_euclidean_space"
   1.100 -  shows "{a<..<b} \<subseteq> {a .. b}"
   1.101 +  shows "box a b \<subseteq> {a .. b}"
   1.102    unfolding subset_eq [unfolded Ball_def] mem_interval
   1.103    by (fast intro: less_imp_le)
   1.104  
   1.105  lemma subset_interval:
   1.106    fixes a :: "'a::ordered_euclidean_space"
   1.107    shows "{c .. d} \<subseteq> {a .. b} \<longleftrightarrow> (\<forall>i\<in>Basis. c\<bullet>i \<le> d\<bullet>i) --> (\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i)" (is ?th1)
   1.108 -    and "{c .. d} \<subseteq> {a<..<b} \<longleftrightarrow> (\<forall>i\<in>Basis. c\<bullet>i \<le> d\<bullet>i) --> (\<forall>i\<in>Basis. a\<bullet>i < c\<bullet>i \<and> d\<bullet>i < b\<bullet>i)" (is ?th2)
   1.109 -    and "{c<..<d} \<subseteq> {a .. b} \<longleftrightarrow> (\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i) --> (\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i)" (is ?th3)
   1.110 -    and "{c<..<d} \<subseteq> {a<..<b} \<longleftrightarrow> (\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i) --> (\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i)" (is ?th4)
   1.111 +    and "{c .. d} \<subseteq> box a b \<longleftrightarrow> (\<forall>i\<in>Basis. c\<bullet>i \<le> d\<bullet>i) --> (\<forall>i\<in>Basis. a\<bullet>i < c\<bullet>i \<and> d\<bullet>i < b\<bullet>i)" (is ?th2)
   1.112 +    and "box c d \<subseteq> {a .. b} \<longleftrightarrow> (\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i) --> (\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i)" (is ?th3)
   1.113 +    and "box c d \<subseteq> box a b \<longleftrightarrow> (\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i) --> (\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i)" (is ?th4)
   1.114  proof -
   1.115    show ?th1
   1.116      unfolding subset_eq and Ball_def and mem_interval
   1.117 @@ -6101,8 +6107,8 @@
   1.118      unfolding subset_eq and Ball_def and mem_interval
   1.119      by (auto intro: le_less_trans less_le_trans order_trans less_imp_le)
   1.120    {
   1.121 -    assume as: "{c<..<d} \<subseteq> {a .. b}" "\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i"
   1.122 -    then have "{c<..<d} \<noteq> {}"
   1.123 +    assume as: "box c d \<subseteq> {a .. b}" "\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i"
   1.124 +    then have "box c d \<noteq> {}"
   1.125        unfolding interval_eq_empty by auto
   1.126      fix i :: 'a
   1.127      assume i: "i \<in> Basis"
   1.128 @@ -6119,7 +6125,7 @@
   1.129            apply (auto simp add: as2)
   1.130            done
   1.131        }
   1.132 -      then have "?x\<in>{c<..<d}"
   1.133 +      then have "?x\<in>box c d"
   1.134          using i unfolding mem_interval by auto
   1.135        moreover
   1.136        have "?x \<notin> {a .. b}"
   1.137 @@ -6145,7 +6151,7 @@
   1.138            apply (auto simp add: as2)
   1.139            done
   1.140        }
   1.141 -      then have "?x\<in>{c<..<d}"
   1.142 +      then have "?x\<in>box c d"
   1.143          unfolding mem_interval by auto
   1.144        moreover
   1.145        have "?x\<notin>{a .. b}"
   1.146 @@ -6171,10 +6177,10 @@
   1.147      apply (erule_tac x=xa in allE, erule_tac x=xa in allE, fastforce)+
   1.148      done
   1.149    {
   1.150 -    assume as: "{c<..<d} \<subseteq> {a<..<b}" "\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i"
   1.151 +    assume as: "box c d \<subseteq> box a b" "\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i"
   1.152      fix i :: 'a
   1.153      assume i:"i\<in>Basis"
   1.154 -    from as(1) have "{c<..<d} \<subseteq> {a..b}"
   1.155 +    from as(1) have "box c d \<subseteq> {a..b}"
   1.156        using interval_open_subset_closed[of a b] by auto
   1.157      then have "a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i"
   1.158        using part1 and as(2) using i by auto
   1.159 @@ -6200,9 +6206,9 @@
   1.160  lemma disjoint_interval:
   1.161    fixes a::"'a::ordered_euclidean_space"
   1.162    shows "{a .. b} \<inter> {c .. d} = {} \<longleftrightarrow> (\<exists>i\<in>Basis. (b\<bullet>i < a\<bullet>i \<or> d\<bullet>i < c\<bullet>i \<or> b\<bullet>i < c\<bullet>i \<or> d\<bullet>i < a\<bullet>i))" (is ?th1)
   1.163 -    and "{a .. b} \<inter> {c<..<d} = {} \<longleftrightarrow> (\<exists>i\<in>Basis. (b\<bullet>i < a\<bullet>i \<or> d\<bullet>i \<le> c\<bullet>i \<or> b\<bullet>i \<le> c\<bullet>i \<or> d\<bullet>i \<le> a\<bullet>i))" (is ?th2)
   1.164 -    and "{a<..<b} \<inter> {c .. d} = {} \<longleftrightarrow> (\<exists>i\<in>Basis. (b\<bullet>i \<le> a\<bullet>i \<or> d\<bullet>i < c\<bullet>i \<or> b\<bullet>i \<le> c\<bullet>i \<or> d\<bullet>i \<le> a\<bullet>i))" (is ?th3)
   1.165 -    and "{a<..<b} \<inter> {c<..<d} = {} \<longleftrightarrow> (\<exists>i\<in>Basis. (b\<bullet>i \<le> a\<bullet>i \<or> d\<bullet>i \<le> c\<bullet>i \<or> b\<bullet>i \<le> c\<bullet>i \<or> d\<bullet>i \<le> a\<bullet>i))" (is ?th4)
   1.166 +    and "{a .. b} \<inter> box c d = {} \<longleftrightarrow> (\<exists>i\<in>Basis. (b\<bullet>i < a\<bullet>i \<or> d\<bullet>i \<le> c\<bullet>i \<or> b\<bullet>i \<le> c\<bullet>i \<or> d\<bullet>i \<le> a\<bullet>i))" (is ?th2)
   1.167 +    and "box a b \<inter> {c .. d} = {} \<longleftrightarrow> (\<exists>i\<in>Basis. (b\<bullet>i \<le> a\<bullet>i \<or> d\<bullet>i < c\<bullet>i \<or> b\<bullet>i \<le> c\<bullet>i \<or> d\<bullet>i \<le> a\<bullet>i))" (is ?th3)
   1.168 +    and "box a b \<inter> box c d = {} \<longleftrightarrow> (\<exists>i\<in>Basis. (b\<bullet>i \<le> a\<bullet>i \<or> d\<bullet>i \<le> c\<bullet>i \<or> b\<bullet>i \<le> c\<bullet>i \<or> d\<bullet>i \<le> a\<bullet>i))" (is ?th4)
   1.169  proof -
   1.170    let ?z = "(\<Sum>i\<in>Basis. (((max (a\<bullet>i) (c\<bullet>i)) + (min (b\<bullet>i) (d\<bullet>i))) / 2) *\<^sub>R i)::'a"
   1.171    have **: "\<And>P Q. (\<And>i :: 'a. i \<in> Basis \<Longrightarrow> Q ?z i \<Longrightarrow> P i) \<Longrightarrow>
   1.172 @@ -6219,14 +6225,14 @@
   1.173  
   1.174  lemma open_interval[intro]:
   1.175    fixes a b :: "'a::ordered_euclidean_space"
   1.176 -  shows "open {a<..<b}"
   1.177 +  shows "open (box a b)"
   1.178  proof -
   1.179    have "open (\<Inter>i\<in>Basis. (\<lambda>x. x\<bullet>i) -` {a\<bullet>i<..<b\<bullet>i})"
   1.180      by (intro open_INT finite_lessThan ballI continuous_open_vimage allI
   1.181        linear_continuous_at open_real_greaterThanLessThan finite_Basis bounded_linear_inner_left)
   1.182 -  also have "(\<Inter>i\<in>Basis. (\<lambda>x. x\<bullet>i) -` {a\<bullet>i<..<b\<bullet>i}) = {a<..<b}"
   1.183 -    by (auto simp add: eucl_less [where 'a='a])
   1.184 -  finally show "open {a<..<b}" .
   1.185 +  also have "(\<Inter>i\<in>Basis. (\<lambda>x. x\<bullet>i) -` {a\<bullet>i<..<b\<bullet>i}) = box a b"
   1.186 +    by (auto simp add: interval)
   1.187 +  finally show "open (box a b)" .
   1.188  qed
   1.189  
   1.190  lemma closed_interval[intro]:
   1.191 @@ -6243,7 +6249,7 @@
   1.192  
   1.193  lemma interior_closed_interval [intro]:
   1.194    fixes a b :: "'a::ordered_euclidean_space"
   1.195 -  shows "interior {a..b} = {a<..<b}" (is "?L = ?R")
   1.196 +  shows "interior {a..b} = box a b" (is "?L = ?R")
   1.197  proof(rule subset_antisym)
   1.198    show "?R \<subseteq> ?L"
   1.199      using interval_open_subset_closed open_interval
   1.200 @@ -6275,7 +6281,7 @@
   1.201          using `e>0` i
   1.202          by (auto simp: inner_diff_left inner_Basis inner_add_left)
   1.203      }
   1.204 -    then have "x \<in> {a<..<b}"
   1.205 +    then have "x \<in> box a b"
   1.206        unfolding mem_interval by auto
   1.207    }
   1.208    then show "?L \<subseteq> ?R" ..
   1.209 @@ -6309,15 +6315,15 @@
   1.210  
   1.211  lemma bounded_interval:
   1.212    fixes a :: "'a::ordered_euclidean_space"
   1.213 -  shows "bounded {a .. b} \<and> bounded {a<..<b}"
   1.214 +  shows "bounded {a .. b} \<and> bounded (box a b)"
   1.215    using bounded_closed_interval[of a b]
   1.216    using interval_open_subset_closed[of a b]
   1.217 -  using bounded_subset[of "{a..b}" "{a<..<b}"]
   1.218 +  using bounded_subset[of "{a..b}" "box a b"]
   1.219    by simp
   1.220  
   1.221  lemma not_interval_univ:
   1.222    fixes a :: "'a::ordered_euclidean_space"
   1.223 -  shows "{a .. b} \<noteq> UNIV \<and> {a<..<b} \<noteq> UNIV"
   1.224 +  shows "{a .. b} \<noteq> UNIV \<and> box a b \<noteq> UNIV"
   1.225    using bounded_interval[of a b] by auto
   1.226  
   1.227  lemma compact_interval:
   1.228 @@ -6328,8 +6334,8 @@
   1.229  
   1.230  lemma open_interval_midpoint:
   1.231    fixes a :: "'a::ordered_euclidean_space"
   1.232 -  assumes "{a<..<b} \<noteq> {}"
   1.233 -  shows "((1/2) *\<^sub>R (a + b)) \<in> {a<..<b}"
   1.234 +  assumes "box a b \<noteq> {}"
   1.235 +  shows "((1/2) *\<^sub>R (a + b)) \<in> box a b"
   1.236  proof -
   1.237    {
   1.238      fix i :: 'a
   1.239 @@ -6342,10 +6348,10 @@
   1.240  
   1.241  lemma open_closed_interval_convex:
   1.242    fixes x :: "'a::ordered_euclidean_space"
   1.243 -  assumes x: "x \<in> {a<..<b}"
   1.244 +  assumes x: "x \<in> box a b"
   1.245      and y: "y \<in> {a .. b}"
   1.246      and e: "0 < e" "e \<le> 1"
   1.247 -  shows "(e *\<^sub>R x + (1 - e) *\<^sub>R y) \<in> {a<..<b}"
   1.248 +  shows "(e *\<^sub>R x + (1 - e) *\<^sub>R y) \<in> box a b"
   1.249  proof -
   1.250    {
   1.251      fix i :: 'a
   1.252 @@ -6392,14 +6398,11 @@
   1.253  
   1.254  lemma closure_open_interval:
   1.255    fixes a :: "'a::ordered_euclidean_space"
   1.256 -  assumes "{a<..<b} \<noteq> {}"
   1.257 -  shows "closure {a<..<b} = {a .. b}"
   1.258 +  assumes "box a b \<noteq> {}"
   1.259 +  shows "closure (box a b) = {a .. b}"
   1.260  proof -
   1.261 -  have ab: "a < b"
   1.262 -    using assms[unfolded interval_ne_empty]
   1.263 -    apply (subst eucl_less)
   1.264 -    apply auto
   1.265 -    done
   1.266 +  have ab: "a <e b"
   1.267 +    using assms by (simp add: eucl_less_def interval_ne_empty)
   1.268    let ?c = "(1 / 2) *\<^sub>R (a + b)"
   1.269    {
   1.270      fix x
   1.271 @@ -6407,15 +6410,15 @@
   1.272      def f \<equiv> "\<lambda>n::nat. x + (inverse (real n + 1)) *\<^sub>R (?c - x)"
   1.273      {
   1.274        fix n
   1.275 -      assume fn: "f n < b \<longrightarrow> a < f n \<longrightarrow> f n = x" and xc: "x \<noteq> ?c"
   1.276 +      assume fn: "f n <e b \<longrightarrow> a <e f n \<longrightarrow> f n = x" and xc: "x \<noteq> ?c"
   1.277        have *: "0 < inverse (real n + 1)" "inverse (real n + 1) \<le> 1"
   1.278          unfolding inverse_le_1_iff by auto
   1.279        have "(inverse (real n + 1)) *\<^sub>R ((1 / 2) *\<^sub>R (a + b)) + (1 - inverse (real n + 1)) *\<^sub>R x =
   1.280          x + (inverse (real n + 1)) *\<^sub>R (((1 / 2) *\<^sub>R (a + b)) - x)"
   1.281          by (auto simp add: algebra_simps)
   1.282 -      then have "f n < b" and "a < f n"
   1.283 +      then have "f n <e b" and "a <e f n"
   1.284          using open_closed_interval_convex[OF open_interval_midpoint[OF assms] as *]
   1.285 -        unfolding f_def by auto
   1.286 +        unfolding f_def by (auto simp: interval eucl_less_def)
   1.287        then have False
   1.288          using fn unfolding f_def using xc by auto
   1.289      }
   1.290 @@ -6448,11 +6451,11 @@
   1.291          using tendsto_scaleR [OF _ tendsto_const, of "\<lambda>n::nat. inverse (real n + 1)" 0 sequentially "((1 / 2) *\<^sub>R (a + b) - x)"]
   1.292          by auto
   1.293      }
   1.294 -    ultimately have "x \<in> closure {a<..<b}"
   1.295 +    ultimately have "x \<in> closure (box a b)"
   1.296        using as and open_interval_midpoint[OF assms]
   1.297        unfolding closure_def
   1.298        unfolding islimpt_sequential
   1.299 -      by (cases "x=?c") auto
   1.300 +      by (cases "x=?c") (auto simp: in_box_eucl_less)
   1.301    }
   1.302    then show ?thesis
   1.303      using closure_minimal[OF interval_open_subset_closed closed_interval, of a b] by blast
   1.304 @@ -6461,7 +6464,7 @@
   1.305  lemma bounded_subset_open_interval_symmetric:
   1.306    fixes s::"('a::ordered_euclidean_space) set"
   1.307    assumes "bounded s"
   1.308 -  shows "\<exists>a. s \<subseteq> {-a<..<a}"
   1.309 +  shows "\<exists>a. s \<subseteq> box (-a) a"
   1.310  proof -
   1.311    obtain b where "b>0" and b: "\<forall>x\<in>s. norm x \<le> b"
   1.312      using assms[unfolded bounded_pos] by auto
   1.313 @@ -6478,12 +6481,12 @@
   1.314        by auto
   1.315    }
   1.316    then show ?thesis
   1.317 -    by (auto intro: exI[where x=a] simp add: eucl_less[where 'a='a])
   1.318 +    by (auto intro: exI[where x=a] simp add: interval)
   1.319  qed
   1.320  
   1.321  lemma bounded_subset_open_interval:
   1.322    fixes s :: "('a::ordered_euclidean_space) set"
   1.323 -  shows "bounded s \<Longrightarrow> (\<exists>a b. s \<subseteq> {a<..<b})"
   1.324 +  shows "bounded s \<Longrightarrow> (\<exists>a b. s \<subseteq> box a b)"
   1.325    by (auto dest!: bounded_subset_open_interval_symmetric)
   1.326  
   1.327  lemma bounded_subset_closed_interval_symmetric:
   1.328 @@ -6491,7 +6494,7 @@
   1.329    assumes "bounded s"
   1.330    shows "\<exists>a. s \<subseteq> {-a .. a}"
   1.331  proof -
   1.332 -  obtain a where "s \<subseteq> {- a<..<a}"
   1.333 +  obtain a where "s \<subseteq> box (-a) a"
   1.334      using bounded_subset_open_interval_symmetric[OF assms] by auto
   1.335    then show ?thesis
   1.336      using interval_open_subset_closed[of "-a" a] by auto
   1.337 @@ -6504,13 +6507,13 @@
   1.338  
   1.339  lemma frontier_closed_interval:
   1.340    fixes a b :: "'a::ordered_euclidean_space"
   1.341 -  shows "frontier {a .. b} = {a .. b} - {a<..<b}"
   1.342 +  shows "frontier {a .. b} = {a .. b} - box a b"
   1.343    unfolding frontier_def unfolding interior_closed_interval and closure_closed[OF closed_interval] ..
   1.344  
   1.345  lemma frontier_open_interval:
   1.346    fixes a b :: "'a::ordered_euclidean_space"
   1.347 -  shows "frontier {a<..<b} = (if {a<..<b} = {} then {} else {a .. b} - {a<..<b})"
   1.348 -proof (cases "{a<..<b} = {}")
   1.349 +  shows "frontier (box a b) = (if box a b = {} then {} else {a .. b} - box a b)"
   1.350 +proof (cases "box a b = {}")
   1.351    case True
   1.352    then show ?thesis
   1.353      using frontier_empty by auto
   1.354 @@ -6523,8 +6526,8 @@
   1.355  
   1.356  lemma inter_interval_mixed_eq_empty:
   1.357    fixes a :: "'a::ordered_euclidean_space"
   1.358 -  assumes "{c<..<d} \<noteq> {}"
   1.359 -  shows "{a<..<b} \<inter> {c .. d} = {} \<longleftrightarrow> {a<..<b} \<inter> {c<..<d} = {}"
   1.360 +  assumes "box c d \<noteq> {}"
   1.361 +  shows "box a b \<inter> {c .. d} = {} \<longleftrightarrow> box a b \<inter> box c d = {}"
   1.362    unfolding closure_open_interval[OF assms, symmetric]
   1.363    unfolding open_inter_closure_eq_empty[OF open_interval] ..
   1.364  
   1.365 @@ -6577,7 +6580,7 @@
   1.366    (\<forall>a\<in>s. \<forall>b\<in>s. \<forall>x. (\<forall>i\<in>Basis. ((a\<bullet>i \<le> x\<bullet>i \<and> x\<bullet>i \<le> b\<bullet>i) \<or> (b\<bullet>i \<le> x\<bullet>i \<and> x\<bullet>i \<le> a\<bullet>i))) \<longrightarrow> x \<in> s)"
   1.367  
   1.368  lemma is_interval_interval: "is_interval {a .. b::'a::ordered_euclidean_space}" (is ?th1)
   1.369 -  "is_interval {a<..<b}" (is ?th2) proof -
   1.370 +  "is_interval (box a b)" (is ?th2) proof -
   1.371    show ?th1 ?th2  unfolding is_interval_def mem_interval Ball_def atLeastAtMost_iff
   1.372      by(meson order_trans le_less_trans less_le_trans less_trans)+ qed
   1.373  
   1.374 @@ -6705,13 +6708,13 @@
   1.375  
   1.376  lemma eucl_lessThan_eq_halfspaces:
   1.377    fixes a :: "'a\<Colon>ordered_euclidean_space"
   1.378 -  shows "{..<a} = (\<Inter>i\<in>Basis. {x. x \<bullet> i < a \<bullet> i})"
   1.379 -  by (auto simp: eucl_less[where 'a='a])
   1.380 +  shows "{x. x <e a} = (\<Inter>i\<in>Basis. {x. x \<bullet> i < a \<bullet> i})"
   1.381 +  by (auto simp: eucl_less_def)
   1.382  
   1.383  lemma eucl_greaterThan_eq_halfspaces:
   1.384    fixes a :: "'a\<Colon>ordered_euclidean_space"
   1.385 -  shows "{a<..} = (\<Inter>i\<in>Basis. {x. a \<bullet> i < x \<bullet> i})"
   1.386 -  by (auto simp: eucl_less[where 'a='a])
   1.387 +  shows "{x. a <e x} = (\<Inter>i\<in>Basis. {x. a \<bullet> i < x \<bullet> i})"
   1.388 +  by (auto simp: eucl_less_def)
   1.389  
   1.390  lemma eucl_atMost_eq_halfspaces:
   1.391    fixes a :: "'a\<Colon>ordered_euclidean_space"
   1.392 @@ -6725,12 +6728,12 @@
   1.393  
   1.394  lemma open_eucl_lessThan[simp, intro]:
   1.395    fixes a :: "'a\<Colon>ordered_euclidean_space"
   1.396 -  shows "open {..< a}"
   1.397 +  shows "open {x. x <e a}"
   1.398    by (auto simp: eucl_lessThan_eq_halfspaces open_halfspace_component_lt)
   1.399  
   1.400  lemma open_eucl_greaterThan[simp, intro]:
   1.401    fixes a :: "'a\<Colon>ordered_euclidean_space"
   1.402 -  shows "open {a <..}"
   1.403 +  shows "open {x. a <e x}"
   1.404    by (auto simp: eucl_greaterThan_eq_halfspaces open_halfspace_component_gt)
   1.405  
   1.406  lemma closed_eucl_atMost[simp, intro]:
   1.407 @@ -7101,7 +7104,7 @@
   1.408        by auto
   1.409      then obtain l where "l\<in>s" and l:"(x ---> l) sequentially"
   1.410        using cs[unfolded complete_def, THEN spec[where x="x"]]
   1.411 -      using cauchy_isometric[OF `0<e` s f normf] and cfg and x(1)
   1.412 +      using cauchy_isometric[OF `0 < e` s f normf] and cfg and x(1)
   1.413        by auto
   1.414      then have "\<exists>l\<in>f ` s. (g ---> l) sequentially"
   1.415        using linear_continuous_at[OF f, unfolded continuous_at_sequentially, THEN spec[where x=x], of l]
   1.416 @@ -7628,4 +7631,7 @@
   1.417  
   1.418  declare tendsto_const [intro] (* FIXME: move *)
   1.419  
   1.420 +no_notation
   1.421 +  eucl_less (infix "<e" 50)
   1.422 +
   1.423  end