src/HOL/Analysis/Topology_Euclidean_Space.thy
 author nipkow Sat Dec 29 15:43:53 2018 +0100 (6 months ago) changeset 69529 4ab9657b3257 parent 69516 09bb8f470959 child 69544 5aa5a8d6e5b5 permissions -rw-r--r--
capitalize proper names in lemma names
```     1 (*  Author:     L C Paulson, University of Cambridge
```
```     2     Author:     Amine Chaieb, University of Cambridge
```
```     3     Author:     Robert Himmelmann, TU Muenchen
```
```     4     Author:     Brian Huffman, Portland State University
```
```     5 *)
```
```     6
```
```     7 section \<open>Elementary Topology in Euclidean Space\<close>
```
```     8
```
```     9 theory Topology_Euclidean_Space
```
```    10   imports
```
```    11     Elementary_Topology
```
```    12     Linear_Algebra
```
```    13     Norm_Arith
```
```    14 begin
```
```    15
```
```    16 lemma euclidean_dist_l2:
```
```    17   fixes x y :: "'a :: euclidean_space"
```
```    18   shows "dist x y = L2_set (\<lambda>i. dist (x \<bullet> i) (y \<bullet> i)) Basis"
```
```    19   unfolding dist_norm norm_eq_sqrt_inner L2_set_def
```
```    20   by (subst euclidean_inner) (simp add: power2_eq_square inner_diff_left)
```
```    21
```
```    22 lemma norm_nth_le: "norm (x \<bullet> i) \<le> norm x" if "i \<in> Basis"
```
```    23 proof -
```
```    24   have "(x \<bullet> i)\<^sup>2 = (\<Sum>i\<in>{i}. (x \<bullet> i)\<^sup>2)"
```
```    25     by simp
```
```    26   also have "\<dots> \<le> (\<Sum>i\<in>Basis. (x \<bullet> i)\<^sup>2)"
```
```    27     by (intro sum_mono2) (auto simp: that)
```
```    28   finally show ?thesis
```
```    29     unfolding norm_conv_dist euclidean_dist_l2[of x] L2_set_def
```
```    30     by (auto intro!: real_le_rsqrt)
```
```    31 qed
```
```    32
```
```    33
```
```    34 subsection \<open>Boxes\<close>
```
```    35
```
```    36 abbreviation One :: "'a::euclidean_space"
```
```    37   where "One \<equiv> \<Sum>Basis"
```
```    38
```
```    39 lemma One_non_0: assumes "One = (0::'a::euclidean_space)" shows False
```
```    40 proof -
```
```    41   have "dependent (Basis :: 'a set)"
```
```    42     apply (simp add: dependent_finite)
```
```    43     apply (rule_tac x="\<lambda>i. 1" in exI)
```
```    44     using SOME_Basis apply (auto simp: assms)
```
```    45     done
```
```    46   with independent_Basis show False by force
```
```    47 qed
```
```    48
```
```    49 corollary One_neq_0[iff]: "One \<noteq> 0"
```
```    50   by (metis One_non_0)
```
```    51
```
```    52 corollary Zero_neq_One[iff]: "0 \<noteq> One"
```
```    53   by (metis One_non_0)
```
```    54
```
```    55 definition%important (in euclidean_space) eucl_less (infix "<e" 50)
```
```    56   where "eucl_less a b \<longleftrightarrow> (\<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i)"
```
```    57
```
```    58 definition%important box_eucl_less: "box a b = {x. a <e x \<and> x <e b}"
```
```    59 definition%important "cbox a b = {x. \<forall>i\<in>Basis. a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i}"
```
```    60
```
```    61 lemma box_def: "box a b = {x. \<forall>i\<in>Basis. a \<bullet> i < x \<bullet> i \<and> x \<bullet> i < b \<bullet> i}"
```
```    62   and in_box_eucl_less: "x \<in> box a b \<longleftrightarrow> a <e x \<and> x <e b"
```
```    63   and mem_box: "x \<in> box a b \<longleftrightarrow> (\<forall>i\<in>Basis. a \<bullet> i < x \<bullet> i \<and> x \<bullet> i < b \<bullet> i)"
```
```    64     "x \<in> cbox a b \<longleftrightarrow> (\<forall>i\<in>Basis. a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i)"
```
```    65   by (auto simp: box_eucl_less eucl_less_def cbox_def)
```
```    66
```
```    67 lemma cbox_Pair_eq: "cbox (a, c) (b, d) = cbox a b \<times> cbox c d"
```
```    68   by (force simp: cbox_def Basis_prod_def)
```
```    69
```
```    70 lemma cbox_Pair_iff [iff]: "(x, y) \<in> cbox (a, c) (b, d) \<longleftrightarrow> x \<in> cbox a b \<and> y \<in> cbox c d"
```
```    71   by (force simp: cbox_Pair_eq)
```
```    72
```
```    73 lemma cbox_Complex_eq: "cbox (Complex a c) (Complex b d) = (\<lambda>(x,y). Complex x y) ` (cbox a b \<times> cbox c d)"
```
```    74   apply (auto simp: cbox_def Basis_complex_def)
```
```    75   apply (rule_tac x = "(Re x, Im x)" in image_eqI)
```
```    76   using complex_eq by auto
```
```    77
```
```    78 lemma cbox_Pair_eq_0: "cbox (a, c) (b, d) = {} \<longleftrightarrow> cbox a b = {} \<or> cbox c d = {}"
```
```    79   by (force simp: cbox_Pair_eq)
```
```    80
```
```    81 lemma swap_cbox_Pair [simp]: "prod.swap ` cbox (c, a) (d, b) = cbox (a,c) (b,d)"
```
```    82   by auto
```
```    83
```
```    84 lemma mem_box_real[simp]:
```
```    85   "(x::real) \<in> box a b \<longleftrightarrow> a < x \<and> x < b"
```
```    86   "(x::real) \<in> cbox a b \<longleftrightarrow> a \<le> x \<and> x \<le> b"
```
```    87   by (auto simp: mem_box)
```
```    88
```
```    89 lemma box_real[simp]:
```
```    90   fixes a b:: real
```
```    91   shows "box a b = {a <..< b}" "cbox a b = {a .. b}"
```
```    92   by auto
```
```    93
```
```    94 lemma box_Int_box:
```
```    95   fixes a :: "'a::euclidean_space"
```
```    96   shows "box a b \<inter> box c d =
```
```    97     box (\<Sum>i\<in>Basis. max (a\<bullet>i) (c\<bullet>i) *\<^sub>R i) (\<Sum>i\<in>Basis. min (b\<bullet>i) (d\<bullet>i) *\<^sub>R i)"
```
```    98   unfolding set_eq_iff and Int_iff and mem_box by auto
```
```    99
```
```   100 lemma rational_boxes:
```
```   101   fixes x :: "'a::euclidean_space"
```
```   102   assumes "e > 0"
```
```   103   shows "\<exists>a b. (\<forall>i\<in>Basis. a \<bullet> i \<in> \<rat> \<and> b \<bullet> i \<in> \<rat>) \<and> x \<in> box a b \<and> box a b \<subseteq> ball x e"
```
```   104 proof -
```
```   105   define e' where "e' = e / (2 * sqrt (real (DIM ('a))))"
```
```   106   then have e: "e' > 0"
```
```   107     using assms by (auto simp: DIM_positive)
```
```   108   have "\<forall>i. \<exists>y. y \<in> \<rat> \<and> y < x \<bullet> i \<and> x \<bullet> i - y < e'" (is "\<forall>i. ?th i")
```
```   109   proof
```
```   110     fix i
```
```   111     from Rats_dense_in_real[of "x \<bullet> i - e'" "x \<bullet> i"] e
```
```   112     show "?th i" by auto
```
```   113   qed
```
```   114   from choice[OF this] obtain a where
```
```   115     a: "\<forall>xa. a xa \<in> \<rat> \<and> a xa < x \<bullet> xa \<and> x \<bullet> xa - a xa < e'" ..
```
```   116   have "\<forall>i. \<exists>y. y \<in> \<rat> \<and> x \<bullet> i < y \<and> y - x \<bullet> i < e'" (is "\<forall>i. ?th i")
```
```   117   proof
```
```   118     fix i
```
```   119     from Rats_dense_in_real[of "x \<bullet> i" "x \<bullet> i + e'"] e
```
```   120     show "?th i" by auto
```
```   121   qed
```
```   122   from choice[OF this] obtain b where
```
```   123     b: "\<forall>xa. b xa \<in> \<rat> \<and> x \<bullet> xa < b xa \<and> b xa - x \<bullet> xa < e'" ..
```
```   124   let ?a = "\<Sum>i\<in>Basis. a i *\<^sub>R i" and ?b = "\<Sum>i\<in>Basis. b i *\<^sub>R i"
```
```   125   show ?thesis
```
```   126   proof (rule exI[of _ ?a], rule exI[of _ ?b], safe)
```
```   127     fix y :: 'a
```
```   128     assume *: "y \<in> box ?a ?b"
```
```   129     have "dist x y = sqrt (\<Sum>i\<in>Basis. (dist (x \<bullet> i) (y \<bullet> i))\<^sup>2)"
```
```   130       unfolding L2_set_def[symmetric] by (rule euclidean_dist_l2)
```
```   131     also have "\<dots> < sqrt (\<Sum>(i::'a)\<in>Basis. e^2 / real (DIM('a)))"
```
```   132     proof (rule real_sqrt_less_mono, rule sum_strict_mono)
```
```   133       fix i :: "'a"
```
```   134       assume i: "i \<in> Basis"
```
```   135       have "a i < y\<bullet>i \<and> y\<bullet>i < b i"
```
```   136         using * i by (auto simp: box_def)
```
```   137       moreover have "a i < x\<bullet>i" "x\<bullet>i - a i < e'"
```
```   138         using a by auto
```
```   139       moreover have "x\<bullet>i < b i" "b i - x\<bullet>i < e'"
```
```   140         using b by auto
```
```   141       ultimately have "\<bar>x\<bullet>i - y\<bullet>i\<bar> < 2 * e'"
```
```   142         by auto
```
```   143       then have "dist (x \<bullet> i) (y \<bullet> i) < e/sqrt (real (DIM('a)))"
```
```   144         unfolding e'_def by (auto simp: dist_real_def)
```
```   145       then have "(dist (x \<bullet> i) (y \<bullet> i))\<^sup>2 < (e/sqrt (real (DIM('a))))\<^sup>2"
```
```   146         by (rule power_strict_mono) auto
```
```   147       then show "(dist (x \<bullet> i) (y \<bullet> i))\<^sup>2 < e\<^sup>2 / real DIM('a)"
```
```   148         by (simp add: power_divide)
```
```   149     qed auto
```
```   150     also have "\<dots> = e"
```
```   151       using \<open>0 < e\<close> by simp
```
```   152     finally show "y \<in> ball x e"
```
```   153       by (auto simp: ball_def)
```
```   154   qed (insert a b, auto simp: box_def)
```
```   155 qed
```
```   156
```
```   157 lemma open_UNION_box:
```
```   158   fixes M :: "'a::euclidean_space set"
```
```   159   assumes "open M"
```
```   160   defines "a' \<equiv> \<lambda>f :: 'a \<Rightarrow> real \<times> real. (\<Sum>(i::'a)\<in>Basis. fst (f i) *\<^sub>R i)"
```
```   161   defines "b' \<equiv> \<lambda>f :: 'a \<Rightarrow> real \<times> real. (\<Sum>(i::'a)\<in>Basis. snd (f i) *\<^sub>R i)"
```
```   162   defines "I \<equiv> {f\<in>Basis \<rightarrow>\<^sub>E \<rat> \<times> \<rat>. box (a' f) (b' f) \<subseteq> M}"
```
```   163   shows "M = (\<Union>f\<in>I. box (a' f) (b' f))"
```
```   164 proof -
```
```   165   have "x \<in> (\<Union>f\<in>I. box (a' f) (b' f))" if "x \<in> M" for x
```
```   166   proof -
```
```   167     obtain e where e: "e > 0" "ball x e \<subseteq> M"
```
```   168       using openE[OF \<open>open M\<close> \<open>x \<in> M\<close>] by auto
```
```   169     moreover obtain a b where ab:
```
```   170       "x \<in> box a b"
```
```   171       "\<forall>i \<in> Basis. a \<bullet> i \<in> \<rat>"
```
```   172       "\<forall>i\<in>Basis. b \<bullet> i \<in> \<rat>"
```
```   173       "box a b \<subseteq> ball x e"
```
```   174       using rational_boxes[OF e(1)] by metis
```
```   175     ultimately show ?thesis
```
```   176        by (intro UN_I[of "\<lambda>i\<in>Basis. (a \<bullet> i, b \<bullet> i)"])
```
```   177           (auto simp: euclidean_representation I_def a'_def b'_def)
```
```   178   qed
```
```   179   then show ?thesis by (auto simp: I_def)
```
```   180 qed
```
```   181
```
```   182 corollary open_countable_Union_open_box:
```
```   183   fixes S :: "'a :: euclidean_space set"
```
```   184   assumes "open S"
```
```   185   obtains \<D> where "countable \<D>" "\<D> \<subseteq> Pow S" "\<And>X. X \<in> \<D> \<Longrightarrow> \<exists>a b. X = box a b" "\<Union>\<D> = S"
```
```   186 proof -
```
```   187   let ?a = "\<lambda>f. (\<Sum>(i::'a)\<in>Basis. fst (f i) *\<^sub>R i)"
```
```   188   let ?b = "\<lambda>f. (\<Sum>(i::'a)\<in>Basis. snd (f i) *\<^sub>R i)"
```
```   189   let ?I = "{f\<in>Basis \<rightarrow>\<^sub>E \<rat> \<times> \<rat>. box (?a f) (?b f) \<subseteq> S}"
```
```   190   let ?\<D> = "(\<lambda>f. box (?a f) (?b f)) ` ?I"
```
```   191   show ?thesis
```
```   192   proof
```
```   193     have "countable ?I"
```
```   194       by (simp add: countable_PiE countable_rat)
```
```   195     then show "countable ?\<D>"
```
```   196       by blast
```
```   197     show "\<Union>?\<D> = S"
```
```   198       using open_UNION_box [OF assms] by metis
```
```   199   qed auto
```
```   200 qed
```
```   201
```
```   202 lemma rational_cboxes:
```
```   203   fixes x :: "'a::euclidean_space"
```
```   204   assumes "e > 0"
```
```   205   shows "\<exists>a b. (\<forall>i\<in>Basis. a \<bullet> i \<in> \<rat> \<and> b \<bullet> i \<in> \<rat>) \<and> x \<in> cbox a b \<and> cbox a b \<subseteq> ball x e"
```
```   206 proof -
```
```   207   define e' where "e' = e / (2 * sqrt (real (DIM ('a))))"
```
```   208   then have e: "e' > 0"
```
```   209     using assms by auto
```
```   210   have "\<forall>i. \<exists>y. y \<in> \<rat> \<and> y < x \<bullet> i \<and> x \<bullet> i - y < e'" (is "\<forall>i. ?th i")
```
```   211   proof
```
```   212     fix i
```
```   213     from Rats_dense_in_real[of "x \<bullet> i - e'" "x \<bullet> i"] e
```
```   214     show "?th i" by auto
```
```   215   qed
```
```   216   from choice[OF this] obtain a where
```
```   217     a: "\<forall>u. a u \<in> \<rat> \<and> a u < x \<bullet> u \<and> x \<bullet> u - a u < e'" ..
```
```   218   have "\<forall>i. \<exists>y. y \<in> \<rat> \<and> x \<bullet> i < y \<and> y - x \<bullet> i < e'" (is "\<forall>i. ?th i")
```
```   219   proof
```
```   220     fix i
```
```   221     from Rats_dense_in_real[of "x \<bullet> i" "x \<bullet> i + e'"] e
```
```   222     show "?th i" by auto
```
```   223   qed
```
```   224   from choice[OF this] obtain b where
```
```   225     b: "\<forall>u. b u \<in> \<rat> \<and> x \<bullet> u < b u \<and> b u - x \<bullet> u < e'" ..
```
```   226   let ?a = "\<Sum>i\<in>Basis. a i *\<^sub>R i" and ?b = "\<Sum>i\<in>Basis. b i *\<^sub>R i"
```
```   227   show ?thesis
```
```   228   proof (rule exI[of _ ?a], rule exI[of _ ?b], safe)
```
```   229     fix y :: 'a
```
```   230     assume *: "y \<in> cbox ?a ?b"
```
```   231     have "dist x y = sqrt (\<Sum>i\<in>Basis. (dist (x \<bullet> i) (y \<bullet> i))\<^sup>2)"
```
```   232       unfolding L2_set_def[symmetric] by (rule euclidean_dist_l2)
```
```   233     also have "\<dots> < sqrt (\<Sum>(i::'a)\<in>Basis. e^2 / real (DIM('a)))"
```
```   234     proof (rule real_sqrt_less_mono, rule sum_strict_mono)
```
```   235       fix i :: "'a"
```
```   236       assume i: "i \<in> Basis"
```
```   237       have "a i \<le> y\<bullet>i \<and> y\<bullet>i \<le> b i"
```
```   238         using * i by (auto simp: cbox_def)
```
```   239       moreover have "a i < x\<bullet>i" "x\<bullet>i - a i < e'"
```
```   240         using a by auto
```
```   241       moreover have "x\<bullet>i < b i" "b i - x\<bullet>i < e'"
```
```   242         using b by auto
```
```   243       ultimately have "\<bar>x\<bullet>i - y\<bullet>i\<bar> < 2 * e'"
```
```   244         by auto
```
```   245       then have "dist (x \<bullet> i) (y \<bullet> i) < e/sqrt (real (DIM('a)))"
```
```   246         unfolding e'_def by (auto simp: dist_real_def)
```
```   247       then have "(dist (x \<bullet> i) (y \<bullet> i))\<^sup>2 < (e/sqrt (real (DIM('a))))\<^sup>2"
```
```   248         by (rule power_strict_mono) auto
```
```   249       then show "(dist (x \<bullet> i) (y \<bullet> i))\<^sup>2 < e\<^sup>2 / real DIM('a)"
```
```   250         by (simp add: power_divide)
```
```   251     qed auto
```
```   252     also have "\<dots> = e"
```
```   253       using \<open>0 < e\<close> by simp
```
```   254     finally show "y \<in> ball x e"
```
```   255       by (auto simp: ball_def)
```
```   256   next
```
```   257     show "x \<in> cbox (\<Sum>i\<in>Basis. a i *\<^sub>R i) (\<Sum>i\<in>Basis. b i *\<^sub>R i)"
```
```   258       using a b less_imp_le by (auto simp: cbox_def)
```
```   259   qed (use a b cbox_def in auto)
```
```   260 qed
```
```   261
```
```   262 lemma open_UNION_cbox:
```
```   263   fixes M :: "'a::euclidean_space set"
```
```   264   assumes "open M"
```
```   265   defines "a' \<equiv> \<lambda>f. (\<Sum>(i::'a)\<in>Basis. fst (f i) *\<^sub>R i)"
```
```   266   defines "b' \<equiv> \<lambda>f. (\<Sum>(i::'a)\<in>Basis. snd (f i) *\<^sub>R i)"
```
```   267   defines "I \<equiv> {f\<in>Basis \<rightarrow>\<^sub>E \<rat> \<times> \<rat>. cbox (a' f) (b' f) \<subseteq> M}"
```
```   268   shows "M = (\<Union>f\<in>I. cbox (a' f) (b' f))"
```
```   269 proof -
```
```   270   have "x \<in> (\<Union>f\<in>I. cbox (a' f) (b' f))" if "x \<in> M" for x
```
```   271   proof -
```
```   272     obtain e where e: "e > 0" "ball x e \<subseteq> M"
```
```   273       using openE[OF \<open>open M\<close> \<open>x \<in> M\<close>] by auto
```
```   274     moreover obtain a b where ab: "x \<in> cbox a b" "\<forall>i \<in> Basis. a \<bullet> i \<in> \<rat>"
```
```   275                                   "\<forall>i \<in> Basis. b \<bullet> i \<in> \<rat>" "cbox a b \<subseteq> ball x e"
```
```   276       using rational_cboxes[OF e(1)] by metis
```
```   277     ultimately show ?thesis
```
```   278        by (intro UN_I[of "\<lambda>i\<in>Basis. (a \<bullet> i, b \<bullet> i)"])
```
```   279           (auto simp: euclidean_representation I_def a'_def b'_def)
```
```   280   qed
```
```   281   then show ?thesis by (auto simp: I_def)
```
```   282 qed
```
```   283
```
```   284 corollary open_countable_Union_open_cbox:
```
```   285   fixes S :: "'a :: euclidean_space set"
```
```   286   assumes "open S"
```
```   287   obtains \<D> where "countable \<D>" "\<D> \<subseteq> Pow S" "\<And>X. X \<in> \<D> \<Longrightarrow> \<exists>a b. X = cbox a b" "\<Union>\<D> = S"
```
```   288 proof -
```
```   289   let ?a = "\<lambda>f. (\<Sum>(i::'a)\<in>Basis. fst (f i) *\<^sub>R i)"
```
```   290   let ?b = "\<lambda>f. (\<Sum>(i::'a)\<in>Basis. snd (f i) *\<^sub>R i)"
```
```   291   let ?I = "{f\<in>Basis \<rightarrow>\<^sub>E \<rat> \<times> \<rat>. cbox (?a f) (?b f) \<subseteq> S}"
```
```   292   let ?\<D> = "(\<lambda>f. cbox (?a f) (?b f)) ` ?I"
```
```   293   show ?thesis
```
```   294   proof
```
```   295     have "countable ?I"
```
```   296       by (simp add: countable_PiE countable_rat)
```
```   297     then show "countable ?\<D>"
```
```   298       by blast
```
```   299     show "\<Union>?\<D> = S"
```
```   300       using open_UNION_cbox [OF assms] by metis
```
```   301   qed auto
```
```   302 qed
```
```   303
```
```   304 lemma box_eq_empty:
```
```   305   fixes a :: "'a::euclidean_space"
```
```   306   shows "(box a b = {} \<longleftrightarrow> (\<exists>i\<in>Basis. b\<bullet>i \<le> a\<bullet>i))" (is ?th1)
```
```   307     and "(cbox a b = {} \<longleftrightarrow> (\<exists>i\<in>Basis. b\<bullet>i < a\<bullet>i))" (is ?th2)
```
```   308 proof -
```
```   309   {
```
```   310     fix i x
```
```   311     assume i: "i\<in>Basis" and as:"b\<bullet>i \<le> a\<bullet>i" and x:"x\<in>box a b"
```
```   312     then have "a \<bullet> i < x \<bullet> i \<and> x \<bullet> i < b \<bullet> i"
```
```   313       unfolding mem_box by (auto simp: box_def)
```
```   314     then have "a\<bullet>i < b\<bullet>i" by auto
```
```   315     then have False using as by auto
```
```   316   }
```
```   317   moreover
```
```   318   {
```
```   319     assume as: "\<forall>i\<in>Basis. \<not> (b\<bullet>i \<le> a\<bullet>i)"
```
```   320     let ?x = "(1/2) *\<^sub>R (a + b)"
```
```   321     {
```
```   322       fix i :: 'a
```
```   323       assume i: "i \<in> Basis"
```
```   324       have "a\<bullet>i < b\<bullet>i"
```
```   325         using as[THEN bspec[where x=i]] i by auto
```
```   326       then have "a\<bullet>i < ((1/2) *\<^sub>R (a+b)) \<bullet> i" "((1/2) *\<^sub>R (a+b)) \<bullet> i < b\<bullet>i"
```
```   327         by (auto simp: inner_add_left)
```
```   328     }
```
```   329     then have "box a b \<noteq> {}"
```
```   330       using mem_box(1)[of "?x" a b] by auto
```
```   331   }
```
```   332   ultimately show ?th1 by blast
```
```   333
```
```   334   {
```
```   335     fix i x
```
```   336     assume i: "i \<in> Basis" and as:"b\<bullet>i < a\<bullet>i" and x:"x\<in>cbox a b"
```
```   337     then have "a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i"
```
```   338       unfolding mem_box by auto
```
```   339     then have "a\<bullet>i \<le> b\<bullet>i" by auto
```
```   340     then have False using as by auto
```
```   341   }
```
```   342   moreover
```
```   343   {
```
```   344     assume as:"\<forall>i\<in>Basis. \<not> (b\<bullet>i < a\<bullet>i)"
```
```   345     let ?x = "(1/2) *\<^sub>R (a + b)"
```
```   346     {
```
```   347       fix i :: 'a
```
```   348       assume i:"i \<in> Basis"
```
```   349       have "a\<bullet>i \<le> b\<bullet>i"
```
```   350         using as[THEN bspec[where x=i]] i by auto
```
```   351       then have "a\<bullet>i \<le> ((1/2) *\<^sub>R (a+b)) \<bullet> i" "((1/2) *\<^sub>R (a+b)) \<bullet> i \<le> b\<bullet>i"
```
```   352         by (auto simp: inner_add_left)
```
```   353     }
```
```   354     then have "cbox a b \<noteq> {}"
```
```   355       using mem_box(2)[of "?x" a b] by auto
```
```   356   }
```
```   357   ultimately show ?th2 by blast
```
```   358 qed
```
```   359
```
```   360 lemma box_ne_empty:
```
```   361   fixes a :: "'a::euclidean_space"
```
```   362   shows "cbox a b \<noteq> {} \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i)"
```
```   363   and "box a b \<noteq> {} \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i)"
```
```   364   unfolding box_eq_empty[of a b] by fastforce+
```
```   365
```
```   366 lemma
```
```   367   fixes a :: "'a::euclidean_space"
```
```   368   shows cbox_sing [simp]: "cbox a a = {a}"
```
```   369     and box_sing [simp]: "box a a = {}"
```
```   370   unfolding set_eq_iff mem_box eq_iff [symmetric]
```
```   371   by (auto intro!: euclidean_eqI[where 'a='a])
```
```   372      (metis all_not_in_conv nonempty_Basis)
```
```   373
```
```   374 lemma subset_box_imp:
```
```   375   fixes a :: "'a::euclidean_space"
```
```   376   shows "(\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i) \<Longrightarrow> cbox c d \<subseteq> cbox a b"
```
```   377     and "(\<forall>i\<in>Basis. a\<bullet>i < c\<bullet>i \<and> d\<bullet>i < b\<bullet>i) \<Longrightarrow> cbox c d \<subseteq> box a b"
```
```   378     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> cbox a b"
```
```   379      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"
```
```   380   unfolding subset_eq[unfolded Ball_def] unfolding mem_box
```
```   381   by (best intro: order_trans less_le_trans le_less_trans less_imp_le)+
```
```   382
```
```   383 lemma box_subset_cbox:
```
```   384   fixes a :: "'a::euclidean_space"
```
```   385   shows "box a b \<subseteq> cbox a b"
```
```   386   unfolding subset_eq [unfolded Ball_def] mem_box
```
```   387   by (fast intro: less_imp_le)
```
```   388
```
```   389 lemma subset_box:
```
```   390   fixes a :: "'a::euclidean_space"
```
```   391   shows "cbox c d \<subseteq> cbox a b \<longleftrightarrow> (\<forall>i\<in>Basis. c\<bullet>i \<le> d\<bullet>i) \<longrightarrow> (\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i)" (is ?th1)
```
```   392     and "cbox c d \<subseteq> box a b \<longleftrightarrow> (\<forall>i\<in>Basis. c\<bullet>i \<le> d\<bullet>i) \<longrightarrow> (\<forall>i\<in>Basis. a\<bullet>i < c\<bullet>i \<and> d\<bullet>i < b\<bullet>i)" (is ?th2)
```
```   393     and "box c d \<subseteq> cbox a b \<longleftrightarrow> (\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i) \<longrightarrow> (\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i)" (is ?th3)
```
```   394     and "box c d \<subseteq> box a b \<longleftrightarrow> (\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i) \<longrightarrow> (\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i)" (is ?th4)
```
```   395 proof -
```
```   396   let ?lesscd = "\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i"
```
```   397   let ?lerhs = "\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i"
```
```   398   show ?th1 ?th2
```
```   399     by (fastforce simp: mem_box)+
```
```   400   have acdb: "a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i"
```
```   401     if i: "i \<in> Basis" and box: "box c d \<subseteq> cbox a b" and cd: "\<And>i. i \<in> Basis \<Longrightarrow> c\<bullet>i < d\<bullet>i" for i
```
```   402   proof -
```
```   403     have "box c d \<noteq> {}"
```
```   404       using that
```
```   405       unfolding box_eq_empty by force
```
```   406     { let ?x = "(\<Sum>j\<in>Basis. (if j=i then ((min (a\<bullet>j) (d\<bullet>j))+c\<bullet>j)/2 else (c\<bullet>j+d\<bullet>j)/2) *\<^sub>R j)::'a"
```
```   407       assume *: "a\<bullet>i > c\<bullet>i"
```
```   408       then have "c \<bullet> j < ?x \<bullet> j \<and> ?x \<bullet> j < d \<bullet> j" if "j \<in> Basis" for j
```
```   409         using cd that by (fastforce simp add: i *)
```
```   410       then have "?x \<in> box c d"
```
```   411         unfolding mem_box by auto
```
```   412       moreover have "?x \<notin> cbox a b"
```
```   413         using i cd * by (force simp: mem_box)
```
```   414       ultimately have False using box by auto
```
```   415     }
```
```   416     then have "a\<bullet>i \<le> c\<bullet>i" by force
```
```   417     moreover
```
```   418     { let ?x = "(\<Sum>j\<in>Basis. (if j=i then ((max (b\<bullet>j) (c\<bullet>j))+d\<bullet>j)/2 else (c\<bullet>j+d\<bullet>j)/2) *\<^sub>R j)::'a"
```
```   419       assume *: "b\<bullet>i < d\<bullet>i"
```
```   420       then have "d \<bullet> j > ?x \<bullet> j \<and> ?x \<bullet> j > c \<bullet> j" if "j \<in> Basis" for j
```
```   421         using cd that by (fastforce simp add: i *)
```
```   422       then have "?x \<in> box c d"
```
```   423         unfolding mem_box by auto
```
```   424       moreover have "?x \<notin> cbox a b"
```
```   425         using i cd * by (force simp: mem_box)
```
```   426       ultimately have False using box by auto
```
```   427     }
```
```   428     then have "b\<bullet>i \<ge> d\<bullet>i" by (rule ccontr) auto
```
```   429     ultimately show ?thesis by auto
```
```   430   qed
```
```   431   show ?th3
```
```   432     using acdb by (fastforce simp add: mem_box)
```
```   433   have acdb': "a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i"
```
```   434     if "i \<in> Basis" "box c d \<subseteq> box a b" "\<And>i. i \<in> Basis \<Longrightarrow> c\<bullet>i < d\<bullet>i" for i
```
```   435       using box_subset_cbox[of a b] that acdb by auto
```
```   436   show ?th4
```
```   437     using acdb' by (fastforce simp add: mem_box)
```
```   438 qed
```
```   439
```
```   440 lemma eq_cbox: "cbox a b = cbox c d \<longleftrightarrow> cbox a b = {} \<and> cbox c d = {} \<or> a = c \<and> b = d"
```
```   441       (is "?lhs = ?rhs")
```
```   442 proof
```
```   443   assume ?lhs
```
```   444   then have "cbox a b \<subseteq> cbox c d" "cbox c d \<subseteq> cbox a b"
```
```   445     by auto
```
```   446   then show ?rhs
```
```   447     by (force simp: subset_box box_eq_empty intro: antisym euclidean_eqI)
```
```   448 next
```
```   449   assume ?rhs
```
```   450   then show ?lhs
```
```   451     by force
```
```   452 qed
```
```   453
```
```   454 lemma eq_cbox_box [simp]: "cbox a b = box c d \<longleftrightarrow> cbox a b = {} \<and> box c d = {}"
```
```   455   (is "?lhs \<longleftrightarrow> ?rhs")
```
```   456 proof
```
```   457   assume L: ?lhs
```
```   458   then have "cbox a b \<subseteq> box c d" "box c d \<subseteq> cbox a b"
```
```   459     by auto
```
```   460   then show ?rhs
```
```   461     apply (simp add: subset_box)
```
```   462     using L box_ne_empty box_sing apply (fastforce simp add:)
```
```   463     done
```
```   464 qed force
```
```   465
```
```   466 lemma eq_box_cbox [simp]: "box a b = cbox c d \<longleftrightarrow> box a b = {} \<and> cbox c d = {}"
```
```   467   by (metis eq_cbox_box)
```
```   468
```
```   469 lemma eq_box: "box a b = box c d \<longleftrightarrow> box a b = {} \<and> box c d = {} \<or> a = c \<and> b = d"
```
```   470   (is "?lhs \<longleftrightarrow> ?rhs")
```
```   471 proof
```
```   472   assume L: ?lhs
```
```   473   then have "box a b \<subseteq> box c d" "box c d \<subseteq> box a b"
```
```   474     by auto
```
```   475   then show ?rhs
```
```   476     apply (simp add: subset_box)
```
```   477     using box_ne_empty(2) L
```
```   478     apply auto
```
```   479      apply (meson euclidean_eqI less_eq_real_def not_less)+
```
```   480     done
```
```   481 qed force
```
```   482
```
```   483 lemma subset_box_complex:
```
```   484    "cbox a b \<subseteq> cbox c d \<longleftrightarrow>
```
```   485       (Re a \<le> Re b \<and> Im a \<le> Im b) \<longrightarrow> Re a \<ge> Re c \<and> Im a \<ge> Im c \<and> Re b \<le> Re d \<and> Im b \<le> Im d"
```
```   486    "cbox a b \<subseteq> box c d \<longleftrightarrow>
```
```   487       (Re a \<le> Re b \<and> Im a \<le> Im b) \<longrightarrow> Re a > Re c \<and> Im a > Im c \<and> Re b < Re d \<and> Im b < Im d"
```
```   488    "box a b \<subseteq> cbox c d \<longleftrightarrow>
```
```   489       (Re a < Re b \<and> Im a < Im b) \<longrightarrow> Re a \<ge> Re c \<and> Im a \<ge> Im c \<and> Re b \<le> Re d \<and> Im b \<le> Im d"
```
```   490    "box a b \<subseteq> box c d \<longleftrightarrow>
```
```   491       (Re a < Re b \<and> Im a < Im b) \<longrightarrow> Re a \<ge> Re c \<and> Im a \<ge> Im c \<and> Re b \<le> Re d \<and> Im b \<le> Im d"
```
```   492   by (subst subset_box; force simp: Basis_complex_def)+
```
```   493
```
```   494 lemma Int_interval:
```
```   495   fixes a :: "'a::euclidean_space"
```
```   496   shows "cbox a b \<inter> cbox c d =
```
```   497     cbox (\<Sum>i\<in>Basis. max (a\<bullet>i) (c\<bullet>i) *\<^sub>R i) (\<Sum>i\<in>Basis. min (b\<bullet>i) (d\<bullet>i) *\<^sub>R i)"
```
```   498   unfolding set_eq_iff and Int_iff and mem_box
```
```   499   by auto
```
```   500
```
```   501 lemma disjoint_interval:
```
```   502   fixes a::"'a::euclidean_space"
```
```   503   shows "cbox a b \<inter> cbox 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)
```
```   504     and "cbox 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)
```
```   505     and "box a b \<inter> cbox 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)
```
```   506     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)
```
```   507 proof -
```
```   508   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"
```
```   509   have **: "\<And>P Q. (\<And>i :: 'a. i \<in> Basis \<Longrightarrow> Q ?z i \<Longrightarrow> P i) \<Longrightarrow>
```
```   510       (\<And>i x :: 'a. i \<in> Basis \<Longrightarrow> P i \<Longrightarrow> Q x i) \<Longrightarrow> (\<forall>x. \<exists>i\<in>Basis. Q x i) \<longleftrightarrow> (\<exists>i\<in>Basis. P i)"
```
```   511     by blast
```
```   512   note * = set_eq_iff Int_iff empty_iff mem_box ball_conj_distrib[symmetric] eq_False ball_simps(10)
```
```   513   show ?th1 unfolding * by (intro **) auto
```
```   514   show ?th2 unfolding * by (intro **) auto
```
```   515   show ?th3 unfolding * by (intro **) auto
```
```   516   show ?th4 unfolding * by (intro **) auto
```
```   517 qed
```
```   518
```
```   519 lemma UN_box_eq_UNIV: "(\<Union>i::nat. box (- (real i *\<^sub>R One)) (real i *\<^sub>R One)) = UNIV"
```
```   520 proof -
```
```   521   have "\<bar>x \<bullet> b\<bar> < real_of_int (\<lceil>Max ((\<lambda>b. \<bar>x \<bullet> b\<bar>)`Basis)\<rceil> + 1)"
```
```   522     if [simp]: "b \<in> Basis" for x b :: 'a
```
```   523   proof -
```
```   524     have "\<bar>x \<bullet> b\<bar> \<le> real_of_int \<lceil>\<bar>x \<bullet> b\<bar>\<rceil>"
```
```   525       by (rule le_of_int_ceiling)
```
```   526     also have "\<dots> \<le> real_of_int \<lceil>Max ((\<lambda>b. \<bar>x \<bullet> b\<bar>)`Basis)\<rceil>"
```
```   527       by (auto intro!: ceiling_mono)
```
```   528     also have "\<dots> < real_of_int (\<lceil>Max ((\<lambda>b. \<bar>x \<bullet> b\<bar>)`Basis)\<rceil> + 1)"
```
```   529       by simp
```
```   530     finally show ?thesis .
```
```   531   qed
```
```   532   then have "\<exists>n::nat. \<forall>b\<in>Basis. \<bar>x \<bullet> b\<bar> < real n" for x :: 'a
```
```   533     by (metis order.strict_trans reals_Archimedean2)
```
```   534   moreover have "\<And>x b::'a. \<And>n::nat.  \<bar>x \<bullet> b\<bar> < real n \<longleftrightarrow> - real n < x \<bullet> b \<and> x \<bullet> b < real n"
```
```   535     by auto
```
```   536   ultimately show ?thesis
```
```   537     by (auto simp: box_def inner_sum_left inner_Basis sum.If_cases)
```
```   538 qed
```
```   539
```
```   540
```
```   541 subsection \<open>General Intervals\<close>
```
```   542
```
```   543 definition%important "is_interval (s::('a::euclidean_space) set) \<longleftrightarrow>
```
```   544   (\<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)"
```
```   545
```
```   546 lemma is_interval_1:
```
```   547   "is_interval (s::real set) \<longleftrightarrow> (\<forall>a\<in>s. \<forall>b\<in>s. \<forall> x. a \<le> x \<and> x \<le> b \<longrightarrow> x \<in> s)"
```
```   548   unfolding is_interval_def by auto
```
```   549
```
```   550 lemma is_interval_inter: "is_interval X \<Longrightarrow> is_interval Y \<Longrightarrow> is_interval (X \<inter> Y)"
```
```   551   unfolding is_interval_def
```
```   552   by blast
```
```   553
```
```   554 lemma is_interval_cbox [simp]: "is_interval (cbox a (b::'a::euclidean_space))" (is ?th1)
```
```   555   and is_interval_box [simp]: "is_interval (box a b)" (is ?th2)
```
```   556   unfolding is_interval_def mem_box Ball_def atLeastAtMost_iff
```
```   557   by (meson order_trans le_less_trans less_le_trans less_trans)+
```
```   558
```
```   559 lemma is_interval_empty [iff]: "is_interval {}"
```
```   560   unfolding is_interval_def  by simp
```
```   561
```
```   562 lemma is_interval_univ [iff]: "is_interval UNIV"
```
```   563   unfolding is_interval_def  by simp
```
```   564
```
```   565 lemma mem_is_intervalI:
```
```   566   assumes "is_interval s"
```
```   567     and "a \<in> s" "b \<in> s"
```
```   568     and "\<And>i. i \<in> Basis \<Longrightarrow> 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"
```
```   569   shows "x \<in> s"
```
```   570   by (rule assms(1)[simplified is_interval_def, rule_format, OF assms(2,3,4)])
```
```   571
```
```   572 lemma interval_subst:
```
```   573   fixes S::"'a::euclidean_space set"
```
```   574   assumes "is_interval S"
```
```   575     and "x \<in> S" "y j \<in> S"
```
```   576     and "j \<in> Basis"
```
```   577   shows "(\<Sum>i\<in>Basis. (if i = j then y i \<bullet> i else x \<bullet> i) *\<^sub>R i) \<in> S"
```
```   578   by (rule mem_is_intervalI[OF assms(1,2)]) (auto simp: assms)
```
```   579
```
```   580 lemma mem_box_componentwiseI:
```
```   581   fixes S::"'a::euclidean_space set"
```
```   582   assumes "is_interval S"
```
```   583   assumes "\<And>i. i \<in> Basis \<Longrightarrow> x \<bullet> i \<in> ((\<lambda>x. x \<bullet> i) ` S)"
```
```   584   shows "x \<in> S"
```
```   585 proof -
```
```   586   from assms have "\<forall>i \<in> Basis. \<exists>s \<in> S. x \<bullet> i = s \<bullet> i"
```
```   587     by auto
```
```   588   with finite_Basis obtain s and bs::"'a list"
```
```   589     where s: "\<And>i. i \<in> Basis \<Longrightarrow> x \<bullet> i = s i \<bullet> i" "\<And>i. i \<in> Basis \<Longrightarrow> s i \<in> S"
```
```   590       and bs: "set bs = Basis" "distinct bs"
```
```   591     by (metis finite_distinct_list)
```
```   592   from nonempty_Basis s obtain j where j: "j \<in> Basis" "s j \<in> S"
```
```   593     by blast
```
```   594   define y where
```
```   595     "y = rec_list (s j) (\<lambda>j _ Y. (\<Sum>i\<in>Basis. (if i = j then s i \<bullet> i else Y \<bullet> i) *\<^sub>R i))"
```
```   596   have "x = (\<Sum>i\<in>Basis. (if i \<in> set bs then s i \<bullet> i else s j \<bullet> i) *\<^sub>R i)"
```
```   597     using bs by (auto simp: s(1)[symmetric] euclidean_representation)
```
```   598   also have [symmetric]: "y bs = \<dots>"
```
```   599     using bs(2) bs(1)[THEN equalityD1]
```
```   600     by (induct bs) (auto simp: y_def euclidean_representation intro!: euclidean_eqI[where 'a='a])
```
```   601   also have "y bs \<in> S"
```
```   602     using bs(1)[THEN equalityD1]
```
```   603     apply (induct bs)
```
```   604      apply (auto simp: y_def j)
```
```   605     apply (rule interval_subst[OF assms(1)])
```
```   606       apply (auto simp: s)
```
```   607     done
```
```   608   finally show ?thesis .
```
```   609 qed
```
```   610
```
```   611 lemma cbox01_nonempty [simp]: "cbox 0 One \<noteq> {}"
```
```   612   by (simp add: box_ne_empty inner_Basis inner_sum_left sum_nonneg)
```
```   613
```
```   614 lemma box01_nonempty [simp]: "box 0 One \<noteq> {}"
```
```   615   by (simp add: box_ne_empty inner_Basis inner_sum_left)
```
```   616
```
```   617 lemma empty_as_interval: "{} = cbox One (0::'a::euclidean_space)"
```
```   618   using nonempty_Basis box01_nonempty box_eq_empty(1) box_ne_empty(1) by blast
```
```   619
```
```   620 lemma interval_subset_is_interval:
```
```   621   assumes "is_interval S"
```
```   622   shows "cbox a b \<subseteq> S \<longleftrightarrow> cbox a b = {} \<or> a \<in> S \<and> b \<in> S" (is "?lhs = ?rhs")
```
```   623 proof
```
```   624   assume ?lhs
```
```   625   then show ?rhs  using box_ne_empty(1) mem_box(2) by fastforce
```
```   626 next
```
```   627   assume ?rhs
```
```   628   have "cbox a b \<subseteq> S" if "a \<in> S" "b \<in> S"
```
```   629     using assms unfolding is_interval_def
```
```   630     apply (clarsimp simp add: mem_box)
```
```   631     using that by blast
```
```   632   with \<open>?rhs\<close> show ?lhs
```
```   633     by blast
```
```   634 qed
```
```   635
```
```   636 lemma is_real_interval_union:
```
```   637   "is_interval (X \<union> Y)"
```
```   638   if X: "is_interval X" and Y: "is_interval Y" and I: "(X \<noteq> {} \<Longrightarrow> Y \<noteq> {} \<Longrightarrow> X \<inter> Y \<noteq> {})"
```
```   639   for X Y::"real set"
```
```   640 proof -
```
```   641   consider "X \<noteq> {}" "Y \<noteq> {}" | "X = {}" | "Y = {}" by blast
```
```   642   then show ?thesis
```
```   643   proof cases
```
```   644     case 1
```
```   645     then obtain r where "r \<in> X \<or> X \<inter> Y = {}" "r \<in> Y \<or> X \<inter> Y = {}"
```
```   646       by blast
```
```   647     then show ?thesis
```
```   648       using I 1 X Y unfolding is_interval_1
```
```   649       by (metis (full_types) Un_iff le_cases)
```
```   650   qed (use that in auto)
```
```   651 qed
```
```   652
```
```   653 lemma is_interval_translationI:
```
```   654   assumes "is_interval X"
```
```   655   shows "is_interval ((+) x ` X)"
```
```   656   unfolding is_interval_def
```
```   657 proof safe
```
```   658   fix b d e
```
```   659   assume "b \<in> X" "d \<in> X"
```
```   660     "\<forall>i\<in>Basis. (x + b) \<bullet> i \<le> e \<bullet> i \<and> e \<bullet> i \<le> (x + d) \<bullet> i \<or>
```
```   661        (x + d) \<bullet> i \<le> e \<bullet> i \<and> e \<bullet> i \<le> (x + b) \<bullet> i"
```
```   662   hence "e - x \<in> X"
```
```   663     by (intro mem_is_intervalI[OF assms \<open>b \<in> X\<close> \<open>d \<in> X\<close>, of "e - x"])
```
```   664       (auto simp: algebra_simps)
```
```   665   thus "e \<in> (+) x ` X" by force
```
```   666 qed
```
```   667
```
```   668 lemma is_interval_uminusI:
```
```   669   assumes "is_interval X"
```
```   670   shows "is_interval (uminus ` X)"
```
```   671   unfolding is_interval_def
```
```   672 proof safe
```
```   673   fix b d e
```
```   674   assume "b \<in> X" "d \<in> X"
```
```   675     "\<forall>i\<in>Basis. (- b) \<bullet> i \<le> e \<bullet> i \<and> e \<bullet> i \<le> (- d) \<bullet> i \<or>
```
```   676        (- d) \<bullet> i \<le> e \<bullet> i \<and> e \<bullet> i \<le> (- b) \<bullet> i"
```
```   677   hence "- e \<in> X"
```
```   678     by (intro mem_is_intervalI[OF assms \<open>b \<in> X\<close> \<open>d \<in> X\<close>, of "- e"])
```
```   679       (auto simp: algebra_simps)
```
```   680   thus "e \<in> uminus ` X" by force
```
```   681 qed
```
```   682
```
```   683 lemma is_interval_uminus[simp]: "is_interval (uminus ` x) = is_interval x"
```
```   684   using is_interval_uminusI[of x] is_interval_uminusI[of "uminus ` x"]
```
```   685   by (auto simp: image_image)
```
```   686
```
```   687 lemma is_interval_neg_translationI:
```
```   688   assumes "is_interval X"
```
```   689   shows "is_interval ((-) x ` X)"
```
```   690 proof -
```
```   691   have "(-) x ` X = (+) x ` uminus ` X"
```
```   692     by (force simp: algebra_simps)
```
```   693   also have "is_interval \<dots>"
```
```   694     by (metis is_interval_uminusI is_interval_translationI assms)
```
```   695   finally show ?thesis .
```
```   696 qed
```
```   697
```
```   698 lemma is_interval_translation[simp]:
```
```   699   "is_interval ((+) x ` X) = is_interval X"
```
```   700   using is_interval_neg_translationI[of "(+) x ` X" x]
```
```   701   by (auto intro!: is_interval_translationI simp: image_image)
```
```   702
```
```   703 lemma is_interval_minus_translation[simp]:
```
```   704   shows "is_interval ((-) x ` X) = is_interval X"
```
```   705 proof -
```
```   706   have "(-) x ` X = (+) x ` uminus ` X"
```
```   707     by (force simp: algebra_simps)
```
```   708   also have "is_interval \<dots> = is_interval X"
```
```   709     by simp
```
```   710   finally show ?thesis .
```
```   711 qed
```
```   712
```
```   713 lemma is_interval_minus_translation'[simp]:
```
```   714   shows "is_interval ((\<lambda>x. x - c) ` X) = is_interval X"
```
```   715   using is_interval_translation[of "-c" X]
```
```   716   by (metis image_cong uminus_add_conv_diff)
```
```   717
```
```   718 lemma compact_lemma:
```
```   719   fixes f :: "nat \<Rightarrow> 'a::euclidean_space"
```
```   720   assumes "bounded (range f)"
```
```   721   shows "\<forall>d\<subseteq>Basis. \<exists>l::'a. \<exists> r.
```
```   722     strict_mono r \<and> (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) \<bullet> i) (l \<bullet> i) < e) sequentially)"
```
```   723   by (rule compact_lemma_general[where unproj="\<lambda>e. \<Sum>i\<in>Basis. e i *\<^sub>R i"])
```
```   724      (auto intro!: assms bounded_linear_inner_left bounded_linear_image
```
```   725        simp: euclidean_representation)
```
```   726
```
```   727 instance%important euclidean_space \<subseteq> heine_borel
```
```   728 proof%unimportant
```
```   729   fix f :: "nat \<Rightarrow> 'a"
```
```   730   assume f: "bounded (range f)"
```
```   731   then obtain l::'a and r where r: "strict_mono r"
```
```   732     and l: "\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>Basis. dist (f (r n) \<bullet> i) (l \<bullet> i) < e) sequentially"
```
```   733     using compact_lemma [OF f] by blast
```
```   734   {
```
```   735     fix e::real
```
```   736     assume "e > 0"
```
```   737     hence "e / real_of_nat DIM('a) > 0" by (simp add: DIM_positive)
```
```   738     with l have "eventually (\<lambda>n. \<forall>i\<in>Basis. dist (f (r n) \<bullet> i) (l \<bullet> i) < e / (real_of_nat DIM('a))) sequentially"
```
```   739       by simp
```
```   740     moreover
```
```   741     {
```
```   742       fix n
```
```   743       assume n: "\<forall>i\<in>Basis. dist (f (r n) \<bullet> i) (l \<bullet> i) < e / (real_of_nat DIM('a))"
```
```   744       have "dist (f (r n)) l \<le> (\<Sum>i\<in>Basis. dist (f (r n) \<bullet> i) (l \<bullet> i))"
```
```   745         apply (subst euclidean_dist_l2)
```
```   746         using zero_le_dist
```
```   747         apply (rule L2_set_le_sum)
```
```   748         done
```
```   749       also have "\<dots> < (\<Sum>i\<in>(Basis::'a set). e / (real_of_nat DIM('a)))"
```
```   750         apply (rule sum_strict_mono)
```
```   751         using n
```
```   752         apply auto
```
```   753         done
```
```   754       finally have "dist (f (r n)) l < e"
```
```   755         by auto
```
```   756     }
```
```   757     ultimately have "eventually (\<lambda>n. dist (f (r n)) l < e) sequentially"
```
```   758       by (rule eventually_mono)
```
```   759   }
```
```   760   then have *: "((f \<circ> r) \<longlongrightarrow> l) sequentially"
```
```   761     unfolding o_def tendsto_iff by simp
```
```   762   with r show "\<exists>l r. strict_mono r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
```
```   763     by auto
```
```   764 qed
```
```   765
```
```   766 instance euclidean_space \<subseteq> banach ..
```
```   767
```
```   768
```
```   769 subsubsection%unimportant \<open>Structural rules for pointwise continuity\<close>
```
```   770
```
```   771 lemma continuous_infnorm[continuous_intros]:
```
```   772   "continuous F f \<Longrightarrow> continuous F (\<lambda>x. infnorm (f x))"
```
```   773   unfolding continuous_def by (rule tendsto_infnorm)
```
```   774
```
```   775 lemma continuous_inner[continuous_intros]:
```
```   776   assumes "continuous F f"
```
```   777     and "continuous F g"
```
```   778   shows "continuous F (\<lambda>x. inner (f x) (g x))"
```
```   779   using assms unfolding continuous_def by (rule tendsto_inner)
```
```   780
```
```   781
```
```   782 subsubsection%unimportant \<open>Structural rules for setwise continuity\<close>
```
```   783
```
```   784 lemma continuous_on_infnorm[continuous_intros]:
```
```   785   "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. infnorm (f x))"
```
```   786   unfolding continuous_on by (fast intro: tendsto_infnorm)
```
```   787
```
```   788 lemma continuous_on_inner[continuous_intros]:
```
```   789   fixes g :: "'a::topological_space \<Rightarrow> 'b::real_inner"
```
```   790   assumes "continuous_on s f"
```
```   791     and "continuous_on s g"
```
```   792   shows "continuous_on s (\<lambda>x. inner (f x) (g x))"
```
```   793   using bounded_bilinear_inner assms
```
```   794   by (rule bounded_bilinear.continuous_on)
```
```   795
```
```   796 subsection%unimportant \<open>Intervals\<close>
```
```   797
```
```   798 text \<open>Openness of halfspaces.\<close>
```
```   799
```
```   800 lemma open_halfspace_lt: "open {x. inner a x < b}"
```
```   801   by (simp add: open_Collect_less continuous_on_inner continuous_on_const continuous_on_id)
```
```   802
```
```   803 lemma open_halfspace_gt: "open {x. inner a x > b}"
```
```   804   by (simp add: open_Collect_less continuous_on_inner continuous_on_const continuous_on_id)
```
```   805
```
```   806 lemma open_halfspace_component_lt: "open {x::'a::euclidean_space. x\<bullet>i < a}"
```
```   807   by (simp add: open_Collect_less continuous_on_inner continuous_on_const continuous_on_id)
```
```   808
```
```   809 lemma open_halfspace_component_gt: "open {x::'a::euclidean_space. x\<bullet>i > a}"
```
```   810   by (simp add: open_Collect_less continuous_on_inner continuous_on_const continuous_on_id)
```
```   811
```
```   812 text \<open>This gives a simple derivation of limit component bounds.\<close>
```
```   813
```
```   814 lemma open_box[intro]: "open (box a b)"
```
```   815 proof -
```
```   816   have "open (\<Inter>i\<in>Basis. ((\<bullet>) i) -` {a \<bullet> i <..< b \<bullet> i})"
```
```   817     by (auto intro!: continuous_open_vimage continuous_inner continuous_ident continuous_const)
```
```   818   also have "(\<Inter>i\<in>Basis. ((\<bullet>) i) -` {a \<bullet> i <..< b \<bullet> i}) = box a b"
```
```   819     by (auto simp: box_def inner_commute)
```
```   820   finally show ?thesis .
```
```   821 qed
```
```   822
```
```   823 instance euclidean_space \<subseteq> second_countable_topology
```
```   824 proof
```
```   825   define a where "a f = (\<Sum>i\<in>Basis. fst (f i) *\<^sub>R i)" for f :: "'a \<Rightarrow> real \<times> real"
```
```   826   then have a: "\<And>f. (\<Sum>i\<in>Basis. fst (f i) *\<^sub>R i) = a f"
```
```   827     by simp
```
```   828   define b where "b f = (\<Sum>i\<in>Basis. snd (f i) *\<^sub>R i)" for f :: "'a \<Rightarrow> real \<times> real"
```
```   829   then have b: "\<And>f. (\<Sum>i\<in>Basis. snd (f i) *\<^sub>R i) = b f"
```
```   830     by simp
```
```   831   define B where "B = (\<lambda>f. box (a f) (b f)) ` (Basis \<rightarrow>\<^sub>E (\<rat> \<times> \<rat>))"
```
```   832
```
```   833   have "Ball B open" by (simp add: B_def open_box)
```
```   834   moreover have "(\<forall>A. open A \<longrightarrow> (\<exists>B'\<subseteq>B. \<Union>B' = A))"
```
```   835   proof safe
```
```   836     fix A::"'a set"
```
```   837     assume "open A"
```
```   838     show "\<exists>B'\<subseteq>B. \<Union>B' = A"
```
```   839       apply (rule exI[of _ "{b\<in>B. b \<subseteq> A}"])
```
```   840       apply (subst (3) open_UNION_box[OF \<open>open A\<close>])
```
```   841       apply (auto simp: a b B_def)
```
```   842       done
```
```   843   qed
```
```   844   ultimately
```
```   845   have "topological_basis B"
```
```   846     unfolding topological_basis_def by blast
```
```   847   moreover
```
```   848   have "countable B"
```
```   849     unfolding B_def
```
```   850     by (intro countable_image countable_PiE finite_Basis countable_SIGMA countable_rat)
```
```   851   ultimately show "\<exists>B::'a set set. countable B \<and> open = generate_topology B"
```
```   852     by (blast intro: topological_basis_imp_subbasis)
```
```   853 qed
```
```   854
```
```   855 instance euclidean_space \<subseteq> polish_space ..
```
```   856
```
```   857 lemma closed_cbox[intro]:
```
```   858   fixes a b :: "'a::euclidean_space"
```
```   859   shows "closed (cbox a b)"
```
```   860 proof -
```
```   861   have "closed (\<Inter>i\<in>Basis. (\<lambda>x. x\<bullet>i) -` {a\<bullet>i .. b\<bullet>i})"
```
```   862     by (intro closed_INT ballI continuous_closed_vimage allI
```
```   863       linear_continuous_at closed_real_atLeastAtMost finite_Basis bounded_linear_inner_left)
```
```   864   also have "(\<Inter>i\<in>Basis. (\<lambda>x. x\<bullet>i) -` {a\<bullet>i .. b\<bullet>i}) = cbox a b"
```
```   865     by (auto simp: cbox_def)
```
```   866   finally show "closed (cbox a b)" .
```
```   867 qed
```
```   868
```
```   869 lemma interior_cbox [simp]:
```
```   870   fixes a b :: "'a::euclidean_space"
```
```   871   shows "interior (cbox a b) = box a b" (is "?L = ?R")
```
```   872 proof(rule subset_antisym)
```
```   873   show "?R \<subseteq> ?L"
```
```   874     using box_subset_cbox open_box
```
```   875     by (rule interior_maximal)
```
```   876   {
```
```   877     fix x
```
```   878     assume "x \<in> interior (cbox a b)"
```
```   879     then obtain s where s: "open s" "x \<in> s" "s \<subseteq> cbox a b" ..
```
```   880     then obtain e where "e>0" and e:"\<forall>x'. dist x' x < e \<longrightarrow> x' \<in> cbox a b"
```
```   881       unfolding open_dist and subset_eq by auto
```
```   882     {
```
```   883       fix i :: 'a
```
```   884       assume i: "i \<in> Basis"
```
```   885       have "dist (x - (e / 2) *\<^sub>R i) x < e"
```
```   886         and "dist (x + (e / 2) *\<^sub>R i) x < e"
```
```   887         unfolding dist_norm
```
```   888         apply auto
```
```   889         unfolding norm_minus_cancel
```
```   890         using norm_Basis[OF i] \<open>e>0\<close>
```
```   891         apply auto
```
```   892         done
```
```   893       then have "a \<bullet> i \<le> (x - (e / 2) *\<^sub>R i) \<bullet> i" and "(x + (e / 2) *\<^sub>R i) \<bullet> i \<le> b \<bullet> i"
```
```   894         using e[THEN spec[where x="x - (e/2) *\<^sub>R i"]]
```
```   895           and e[THEN spec[where x="x + (e/2) *\<^sub>R i"]]
```
```   896         unfolding mem_box
```
```   897         using i
```
```   898         by blast+
```
```   899       then have "a \<bullet> i < x \<bullet> i" and "x \<bullet> i < b \<bullet> i"
```
```   900         using \<open>e>0\<close> i
```
```   901         by (auto simp: inner_diff_left inner_Basis inner_add_left)
```
```   902     }
```
```   903     then have "x \<in> box a b"
```
```   904       unfolding mem_box by auto
```
```   905   }
```
```   906   then show "?L \<subseteq> ?R" ..
```
```   907 qed
```
```   908
```
```   909 lemma bounded_cbox [simp]:
```
```   910   fixes a :: "'a::euclidean_space"
```
```   911   shows "bounded (cbox a b)"
```
```   912 proof -
```
```   913   let ?b = "\<Sum>i\<in>Basis. \<bar>a\<bullet>i\<bar> + \<bar>b\<bullet>i\<bar>"
```
```   914   {
```
```   915     fix x :: "'a"
```
```   916     assume "\<And>i. i\<in>Basis \<Longrightarrow> a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i"
```
```   917     then have "(\<Sum>i\<in>Basis. \<bar>x \<bullet> i\<bar>) \<le> ?b"
```
```   918       by (force simp: intro!: sum_mono)
```
```   919     then have "norm x \<le> ?b"
```
```   920       using norm_le_l1[of x] by auto
```
```   921   }
```
```   922   then show ?thesis
```
```   923     unfolding cbox_def bounded_iff by force
```
```   924 qed
```
```   925
```
```   926 lemma bounded_box [simp]:
```
```   927   fixes a :: "'a::euclidean_space"
```
```   928   shows "bounded (box a b)"
```
```   929   using bounded_cbox[of a b] box_subset_cbox[of a b] bounded_subset[of "cbox a b" "box a b"]
```
```   930   by simp
```
```   931
```
```   932 lemma not_interval_UNIV [simp]:
```
```   933   fixes a :: "'a::euclidean_space"
```
```   934   shows "cbox a b \<noteq> UNIV" "box a b \<noteq> UNIV"
```
```   935   using bounded_box[of a b] bounded_cbox[of a b] by force+
```
```   936
```
```   937 lemma not_interval_UNIV2 [simp]:
```
```   938   fixes a :: "'a::euclidean_space"
```
```   939   shows "UNIV \<noteq> cbox a b" "UNIV \<noteq> box a b"
```
```   940   using bounded_box[of a b] bounded_cbox[of a b] by force+
```
```   941
```
```   942 lemma compact_cbox [simp]:
```
```   943   fixes a :: "'a::euclidean_space"
```
```   944   shows "compact (cbox a b)"
```
```   945   using bounded_closed_imp_seq_compact[of "cbox a b"] using bounded_cbox[of a b]
```
```   946   by (auto simp: compact_eq_seq_compact_metric)
```
```   947
```
```   948 lemma box_midpoint:
```
```   949   fixes a :: "'a::euclidean_space"
```
```   950   assumes "box a b \<noteq> {}"
```
```   951   shows "((1/2) *\<^sub>R (a + b)) \<in> box a b"
```
```   952 proof -
```
```   953   have "a \<bullet> i < ((1 / 2) *\<^sub>R (a + b)) \<bullet> i \<and> ((1 / 2) *\<^sub>R (a + b)) \<bullet> i < b \<bullet> i" if "i \<in> Basis" for i
```
```   954     using assms that by (auto simp: inner_add_left box_ne_empty)
```
```   955   then show ?thesis unfolding mem_box by auto
```
```   956 qed
```
```   957
```
```   958 lemma open_cbox_convex:
```
```   959   fixes x :: "'a::euclidean_space"
```
```   960   assumes x: "x \<in> box a b"
```
```   961     and y: "y \<in> cbox a b"
```
```   962     and e: "0 < e" "e \<le> 1"
```
```   963   shows "(e *\<^sub>R x + (1 - e) *\<^sub>R y) \<in> box a b"
```
```   964 proof -
```
```   965   {
```
```   966     fix i :: 'a
```
```   967     assume i: "i \<in> Basis"
```
```   968     have "a \<bullet> i = e * (a \<bullet> i) + (1 - e) * (a \<bullet> i)"
```
```   969       unfolding left_diff_distrib by simp
```
```   970     also have "\<dots> < e * (x \<bullet> i) + (1 - e) * (y \<bullet> i)"
```
```   971     proof (rule add_less_le_mono)
```
```   972       show "e * (a \<bullet> i) < e * (x \<bullet> i)"
```
```   973         using \<open>0 < e\<close> i mem_box(1) x by auto
```
```   974       show "(1 - e) * (a \<bullet> i) \<le> (1 - e) * (y \<bullet> i)"
```
```   975         by (meson diff_ge_0_iff_ge \<open>e \<le> 1\<close> i mem_box(2) mult_left_mono y)
```
```   976     qed
```
```   977     finally have "a \<bullet> i < (e *\<^sub>R x + (1 - e) *\<^sub>R y) \<bullet> i"
```
```   978       unfolding inner_simps by auto
```
```   979     moreover
```
```   980     {
```
```   981       have "b \<bullet> i = e * (b\<bullet>i) + (1 - e) * (b\<bullet>i)"
```
```   982         unfolding left_diff_distrib by simp
```
```   983       also have "\<dots> > e * (x \<bullet> i) + (1 - e) * (y \<bullet> i)"
```
```   984       proof (rule add_less_le_mono)
```
```   985         show "e * (x \<bullet> i) < e * (b \<bullet> i)"
```
```   986           using \<open>0 < e\<close> i mem_box(1) x by auto
```
```   987         show "(1 - e) * (y \<bullet> i) \<le> (1 - e) * (b \<bullet> i)"
```
```   988           by (meson diff_ge_0_iff_ge \<open>e \<le> 1\<close> i mem_box(2) mult_left_mono y)
```
```   989       qed
```
```   990       finally have "(e *\<^sub>R x + (1 - e) *\<^sub>R y) \<bullet> i < b \<bullet> i"
```
```   991         unfolding inner_simps by auto
```
```   992     }
```
```   993     ultimately have "a \<bullet> i < (e *\<^sub>R x + (1 - e) *\<^sub>R y) \<bullet> i \<and> (e *\<^sub>R x + (1 - e) *\<^sub>R y) \<bullet> i < b \<bullet> i"
```
```   994       by auto
```
```   995   }
```
```   996   then show ?thesis
```
```   997     unfolding mem_box by auto
```
```   998 qed
```
```   999
```
```  1000 lemma closure_cbox [simp]: "closure (cbox a b) = cbox a b"
```
```  1001   by (simp add: closed_cbox)
```
```  1002
```
```  1003 lemma closure_box [simp]:
```
```  1004   fixes a :: "'a::euclidean_space"
```
```  1005    assumes "box a b \<noteq> {}"
```
```  1006   shows "closure (box a b) = cbox a b"
```
```  1007 proof -
```
```  1008   have ab: "a <e b"
```
```  1009     using assms by (simp add: eucl_less_def box_ne_empty)
```
```  1010   let ?c = "(1 / 2) *\<^sub>R (a + b)"
```
```  1011   {
```
```  1012     fix x
```
```  1013     assume as:"x \<in> cbox a b"
```
```  1014     define f where [abs_def]: "f n = x + (inverse (real n + 1)) *\<^sub>R (?c - x)" for n
```
```  1015     {
```
```  1016       fix n
```
```  1017       assume fn: "f n <e b \<longrightarrow> a <e f n \<longrightarrow> f n = x" and xc: "x \<noteq> ?c"
```
```  1018       have *: "0 < inverse (real n + 1)" "inverse (real n + 1) \<le> 1"
```
```  1019         unfolding inverse_le_1_iff by auto
```
```  1020       have "(inverse (real n + 1)) *\<^sub>R ((1 / 2) *\<^sub>R (a + b)) + (1 - inverse (real n + 1)) *\<^sub>R x =
```
```  1021         x + (inverse (real n + 1)) *\<^sub>R (((1 / 2) *\<^sub>R (a + b)) - x)"
```
```  1022         by (auto simp: algebra_simps)
```
```  1023       then have "f n <e b" and "a <e f n"
```
```  1024         using open_cbox_convex[OF box_midpoint[OF assms] as *]
```
```  1025         unfolding f_def by (auto simp: box_def eucl_less_def)
```
```  1026       then have False
```
```  1027         using fn unfolding f_def using xc by auto
```
```  1028     }
```
```  1029     moreover
```
```  1030     {
```
```  1031       assume "\<not> (f \<longlongrightarrow> x) sequentially"
```
```  1032       {
```
```  1033         fix e :: real
```
```  1034         assume "e > 0"
```
```  1035         then obtain N :: nat where N: "inverse (real (N + 1)) < e"
```
```  1036           using reals_Archimedean by auto
```
```  1037         have "inverse (real n + 1) < e" if "N \<le> n" for n
```
```  1038           by (auto intro!: that le_less_trans [OF _ N])
```
```  1039         then have "\<exists>N::nat. \<forall>n\<ge>N. inverse (real n + 1) < e" by auto
```
```  1040       }
```
```  1041       then have "((\<lambda>n. inverse (real n + 1)) \<longlongrightarrow> 0) sequentially"
```
```  1042         unfolding lim_sequentially by(auto simp: dist_norm)
```
```  1043       then have "(f \<longlongrightarrow> x) sequentially"
```
```  1044         unfolding f_def
```
```  1045         using tendsto_add[OF tendsto_const, of "\<lambda>n::nat. (inverse (real n + 1)) *\<^sub>R ((1 / 2) *\<^sub>R (a + b) - x)" 0 sequentially x]
```
```  1046         using tendsto_scaleR [OF _ tendsto_const, of "\<lambda>n::nat. inverse (real n + 1)" 0 sequentially "((1 / 2) *\<^sub>R (a + b) - x)"]
```
```  1047         by auto
```
```  1048     }
```
```  1049     ultimately have "x \<in> closure (box a b)"
```
```  1050       using as box_midpoint[OF assms]
```
```  1051       unfolding closure_def islimpt_sequential
```
```  1052       by (cases "x=?c") (auto simp: in_box_eucl_less)
```
```  1053   }
```
```  1054   then show ?thesis
```
```  1055     using closure_minimal[OF box_subset_cbox, of a b] by blast
```
```  1056 qed
```
```  1057
```
```  1058 lemma bounded_subset_box_symmetric:
```
```  1059   fixes S :: "('a::euclidean_space) set"
```
```  1060   assumes "bounded S"
```
```  1061   obtains a where "S \<subseteq> box (-a) a"
```
```  1062 proof -
```
```  1063   obtain b where "b>0" and b: "\<forall>x\<in>S. norm x \<le> b"
```
```  1064     using assms[unfolded bounded_pos] by auto
```
```  1065   define a :: 'a where "a = (\<Sum>i\<in>Basis. (b + 1) *\<^sub>R i)"
```
```  1066   have "(-a)\<bullet>i < x\<bullet>i" and "x\<bullet>i < a\<bullet>i" if "x \<in> S" and i: "i \<in> Basis" for x i
```
```  1067     using b Basis_le_norm[OF i, of x] that by (auto simp: a_def)
```
```  1068   then have "S \<subseteq> box (-a) a"
```
```  1069     by (auto simp: simp add: box_def)
```
```  1070   then show ?thesis ..
```
```  1071 qed
```
```  1072
```
```  1073 lemma bounded_subset_cbox_symmetric:
```
```  1074   fixes S :: "('a::euclidean_space) set"
```
```  1075   assumes "bounded S"
```
```  1076   obtains a where "S \<subseteq> cbox (-a) a"
```
```  1077 proof -
```
```  1078   obtain a where "S \<subseteq> box (-a) a"
```
```  1079     using bounded_subset_box_symmetric[OF assms] by auto
```
```  1080   then show ?thesis
```
```  1081     by (meson box_subset_cbox dual_order.trans that)
```
```  1082 qed
```
```  1083
```
```  1084 lemma frontier_cbox:
```
```  1085   fixes a b :: "'a::euclidean_space"
```
```  1086   shows "frontier (cbox a b) = cbox a b - box a b"
```
```  1087   unfolding frontier_def unfolding interior_cbox and closure_closed[OF closed_cbox] ..
```
```  1088
```
```  1089 lemma frontier_box:
```
```  1090   fixes a b :: "'a::euclidean_space"
```
```  1091   shows "frontier (box a b) = (if box a b = {} then {} else cbox a b - box a b)"
```
```  1092 proof (cases "box a b = {}")
```
```  1093   case True
```
```  1094   then show ?thesis
```
```  1095     using frontier_empty by auto
```
```  1096 next
```
```  1097   case False
```
```  1098   then show ?thesis
```
```  1099     unfolding frontier_def and closure_box[OF False] and interior_open[OF open_box]
```
```  1100     by auto
```
```  1101 qed
```
```  1102
```
```  1103 lemma Int_interval_mixed_eq_empty:
```
```  1104   fixes a :: "'a::euclidean_space"
```
```  1105    assumes "box c d \<noteq> {}"
```
```  1106   shows "box a b \<inter> cbox c d = {} \<longleftrightarrow> box a b \<inter> box c d = {}"
```
```  1107   unfolding closure_box[OF assms, symmetric]
```
```  1108   unfolding open_Int_closure_eq_empty[OF open_box] ..
```
```  1109
```
```  1110 lemma eucl_less_eq_halfspaces:
```
```  1111   fixes a :: "'a::euclidean_space"
```
```  1112   shows "{x. x <e a} = (\<Inter>i\<in>Basis. {x. x \<bullet> i < a \<bullet> i})"
```
```  1113         "{x. a <e x} = (\<Inter>i\<in>Basis. {x. a \<bullet> i < x \<bullet> i})"
```
```  1114   by (auto simp: eucl_less_def)
```
```  1115
```
```  1116 lemma open_Collect_eucl_less[simp, intro]:
```
```  1117   fixes a :: "'a::euclidean_space"
```
```  1118   shows "open {x. x <e a}" "open {x. a <e x}"
```
```  1119   by (auto simp: eucl_less_eq_halfspaces open_halfspace_component_lt open_halfspace_component_gt)
```
```  1120
```
```  1121 no_notation
```
```  1122   eucl_less (infix "<e" 50)
```
```  1123
```
```  1124 end
```