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.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
```