src/HOL/Analysis/Topology_Euclidean_Space.thy
author wenzelm
Mon Mar 25 17:21:26 2019 +0100 (4 weeks ago)
changeset 69981 3dced198b9ec
parent 69922 4a9167f377b0
child 70019 095dce9892e8
permissions -rw-r--r--
more strict AFP properties;
     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 chapter \<open>Vector Analysis\<close>
     8 
     9 theory Topology_Euclidean_Space
    10   imports
    11     Elementary_Normed_Spaces
    12     Linear_Algebra
    13     Norm_Arith
    14 begin
    15 
    16 section \<open>Elementary Topology in Euclidean Space\<close>
    17 
    18 lemma euclidean_dist_l2:
    19   fixes x y :: "'a :: euclidean_space"
    20   shows "dist x y = L2_set (\<lambda>i. dist (x \<bullet> i) (y \<bullet> i)) Basis"
    21   unfolding dist_norm norm_eq_sqrt_inner L2_set_def
    22   by (subst euclidean_inner) (simp add: power2_eq_square inner_diff_left)
    23 
    24 lemma norm_nth_le: "norm (x \<bullet> i) \<le> norm x" if "i \<in> Basis"
    25 proof -
    26   have "(x \<bullet> i)\<^sup>2 = (\<Sum>i\<in>{i}. (x \<bullet> i)\<^sup>2)"
    27     by simp
    28   also have "\<dots> \<le> (\<Sum>i\<in>Basis. (x \<bullet> i)\<^sup>2)"
    29     by (intro sum_mono2) (auto simp: that)
    30   finally show ?thesis
    31     unfolding norm_conv_dist euclidean_dist_l2[of x] L2_set_def
    32     by (auto intro!: real_le_rsqrt)
    33 qed
    34 
    35 
    36 subsection%unimportant\<open>Balls in Euclidean Space\<close>
    37 
    38 lemma cball_subset_cball_iff:
    39   fixes a :: "'a :: euclidean_space"
    40   shows "cball a r \<subseteq> cball a' r' \<longleftrightarrow> dist a a' + r \<le> r' \<or> r < 0"
    41     (is "?lhs \<longleftrightarrow> ?rhs")
    42 proof
    43   assume ?lhs
    44   then show ?rhs
    45   proof (cases "r < 0")
    46     case True
    47     then show ?rhs by simp
    48   next
    49     case False
    50     then have [simp]: "r \<ge> 0" by simp
    51     have "norm (a - a') + r \<le> r'"
    52     proof (cases "a = a'")
    53       case True
    54       then show ?thesis
    55         using subsetD [where c = "a + r *\<^sub>R (SOME i. i \<in> Basis)", OF \<open>?lhs\<close>] subsetD [where c = a, OF \<open>?lhs\<close>]
    56         by (force simp: SOME_Basis dist_norm)
    57     next
    58       case False
    59       have "norm (a' - (a + (r / norm (a - a')) *\<^sub>R (a - a'))) = norm (a' - a - (r / norm (a - a')) *\<^sub>R (a - a'))"
    60         by (simp add: algebra_simps)
    61       also have "... = norm ((-1 - (r / norm (a - a'))) *\<^sub>R (a - a'))"
    62         by (simp add: algebra_simps)
    63       also from \<open>a \<noteq> a'\<close> have "... = \<bar>- norm (a - a') - r\<bar>"
    64         by (simp add: abs_mult_pos field_simps)
    65       finally have [simp]: "norm (a' - (a + (r / norm (a - a')) *\<^sub>R (a - a'))) = \<bar>norm (a - a') + r\<bar>"
    66         by linarith
    67       from \<open>a \<noteq> a'\<close> show ?thesis
    68         using subsetD [where c = "a' + (1 + r / norm(a - a')) *\<^sub>R (a - a')", OF \<open>?lhs\<close>]
    69         by (simp add: dist_norm scaleR_add_left)
    70     qed
    71     then show ?rhs
    72       by (simp add: dist_norm)
    73   qed
    74 next
    75   assume ?rhs
    76   then show ?lhs
    77     by (auto simp: ball_def dist_norm)
    78       (metis add.commute add_le_cancel_right dist_norm dist_triangle3 order_trans)
    79 qed
    80 
    81 lemma cball_subset_ball_iff: "cball a r \<subseteq> ball a' r' \<longleftrightarrow> dist a a' + r < r' \<or> r < 0"
    82   (is "?lhs \<longleftrightarrow> ?rhs")
    83   for a :: "'a::euclidean_space"
    84 proof
    85   assume ?lhs
    86   then show ?rhs
    87   proof (cases "r < 0")
    88     case True then
    89     show ?rhs by simp
    90   next
    91     case False
    92     then have [simp]: "r \<ge> 0" by simp
    93     have "norm (a - a') + r < r'"
    94     proof (cases "a = a'")
    95       case True
    96       then show ?thesis
    97         using subsetD [where c = "a + r *\<^sub>R (SOME i. i \<in> Basis)", OF \<open>?lhs\<close>] subsetD [where c = a, OF \<open>?lhs\<close>]
    98         by (force simp: SOME_Basis dist_norm)
    99     next
   100       case False
   101       have False if "norm (a - a') + r \<ge> r'"
   102       proof -
   103         from that have "\<bar>r' - norm (a - a')\<bar> \<le> r"
   104           by (simp split: abs_split)
   105             (metis \<open>0 \<le> r\<close> \<open>?lhs\<close> centre_in_cball dist_commute dist_norm less_asym mem_ball subset_eq)
   106         then show ?thesis
   107           using subsetD [where c = "a + (r' / norm(a - a') - 1) *\<^sub>R (a - a')", OF \<open>?lhs\<close>] \<open>a \<noteq> a'\<close>
   108           by (simp add: dist_norm field_simps)
   109             (simp add: diff_divide_distrib scaleR_left_diff_distrib)
   110       qed
   111       then show ?thesis by force
   112     qed
   113     then show ?rhs by (simp add: dist_norm)
   114   qed
   115 next
   116   assume ?rhs
   117   then show ?lhs
   118     by (auto simp: ball_def dist_norm)
   119       (metis add.commute add_le_cancel_right dist_norm dist_triangle3 le_less_trans)
   120 qed
   121 
   122 lemma ball_subset_cball_iff: "ball a r \<subseteq> cball a' r' \<longleftrightarrow> dist a a' + r \<le> r' \<or> r \<le> 0"
   123   (is "?lhs = ?rhs")
   124   for a :: "'a::euclidean_space"
   125 proof (cases "r \<le> 0")
   126   case True
   127   then show ?thesis
   128     using dist_not_less_zero less_le_trans by force
   129 next
   130   case False
   131   show ?thesis
   132   proof
   133     assume ?lhs
   134     then have "(cball a r \<subseteq> cball a' r')"
   135       by (metis False closed_cball closure_ball closure_closed closure_mono not_less)
   136     with False show ?rhs
   137       by (fastforce iff: cball_subset_cball_iff)
   138   next
   139     assume ?rhs
   140     with False show ?lhs
   141       using ball_subset_cball cball_subset_cball_iff by blast
   142   qed
   143 qed
   144 
   145 lemma ball_subset_ball_iff:
   146   fixes a :: "'a :: euclidean_space"
   147   shows "ball a r \<subseteq> ball a' r' \<longleftrightarrow> dist a a' + r \<le> r' \<or> r \<le> 0"
   148         (is "?lhs = ?rhs")
   149 proof (cases "r \<le> 0")
   150   case True then show ?thesis
   151     using dist_not_less_zero less_le_trans by force
   152 next
   153   case False show ?thesis
   154   proof
   155     assume ?lhs
   156     then have "0 < r'"
   157       by (metis (no_types) False \<open>?lhs\<close> centre_in_ball dist_norm le_less_trans mem_ball norm_ge_zero not_less subsetD)
   158     then have "(cball a r \<subseteq> cball a' r')"
   159       by (metis False\<open>?lhs\<close> closure_ball closure_mono not_less)
   160     then show ?rhs
   161       using False cball_subset_cball_iff by fastforce
   162   next
   163   assume ?rhs then show ?lhs
   164     apply (auto simp: ball_def)
   165     apply (metis add.commute add_le_cancel_right dist_commute dist_triangle_lt not_le order_trans)
   166     using dist_not_less_zero order.strict_trans2 apply blast
   167     done
   168   qed
   169 qed
   170 
   171 
   172 lemma ball_eq_ball_iff:
   173   fixes x :: "'a :: euclidean_space"
   174   shows "ball x d = ball y e \<longleftrightarrow> d \<le> 0 \<and> e \<le> 0 \<or> x=y \<and> d=e"
   175         (is "?lhs = ?rhs")
   176 proof
   177   assume ?lhs
   178   then show ?rhs
   179   proof (cases "d \<le> 0 \<or> e \<le> 0")
   180     case True
   181       with \<open>?lhs\<close> show ?rhs
   182         by safe (simp_all only: ball_eq_empty [of y e, symmetric] ball_eq_empty [of x d, symmetric])
   183   next
   184     case False
   185     with \<open>?lhs\<close> show ?rhs
   186       apply (auto simp: set_eq_subset ball_subset_ball_iff dist_norm norm_minus_commute algebra_simps)
   187       apply (metis add_le_same_cancel1 le_add_same_cancel1 norm_ge_zero norm_pths(2) order_trans)
   188       apply (metis add_increasing2 add_le_imp_le_right eq_iff norm_ge_zero)
   189       done
   190   qed
   191 next
   192   assume ?rhs then show ?lhs
   193     by (auto simp: set_eq_subset ball_subset_ball_iff)
   194 qed
   195 
   196 lemma cball_eq_cball_iff:
   197   fixes x :: "'a :: euclidean_space"
   198   shows "cball x d = cball y e \<longleftrightarrow> d < 0 \<and> e < 0 \<or> x=y \<and> d=e"
   199         (is "?lhs = ?rhs")
   200 proof
   201   assume ?lhs
   202   then show ?rhs
   203   proof (cases "d < 0 \<or> e < 0")
   204     case True
   205       with \<open>?lhs\<close> show ?rhs
   206         by safe (simp_all only: cball_eq_empty [of y e, symmetric] cball_eq_empty [of x d, symmetric])
   207   next
   208     case False
   209     with \<open>?lhs\<close> show ?rhs
   210       apply (auto simp: set_eq_subset cball_subset_cball_iff dist_norm norm_minus_commute algebra_simps)
   211       apply (metis add_le_same_cancel1 le_add_same_cancel1 norm_ge_zero norm_pths(2) order_trans)
   212       apply (metis add_increasing2 add_le_imp_le_right eq_iff norm_ge_zero)
   213       done
   214   qed
   215 next
   216   assume ?rhs then show ?lhs
   217     by (auto simp: set_eq_subset cball_subset_cball_iff)
   218 qed
   219 
   220 lemma ball_eq_cball_iff:
   221   fixes x :: "'a :: euclidean_space"
   222   shows "ball x d = cball y e \<longleftrightarrow> d \<le> 0 \<and> e < 0" (is "?lhs = ?rhs")
   223 proof
   224   assume ?lhs
   225   then show ?rhs
   226     apply (auto simp: set_eq_subset ball_subset_cball_iff cball_subset_ball_iff algebra_simps)
   227     apply (metis add_increasing2 add_le_cancel_right add_less_same_cancel1 dist_not_less_zero less_le_trans zero_le_dist)
   228     apply (metis add_less_same_cancel1 dist_not_less_zero less_le_trans not_le)
   229     using \<open>?lhs\<close> ball_eq_empty cball_eq_empty apply blast+
   230     done
   231 next
   232   assume ?rhs then show ?lhs by auto
   233 qed
   234 
   235 lemma cball_eq_ball_iff:
   236   fixes x :: "'a :: euclidean_space"
   237   shows "cball x d = ball y e \<longleftrightarrow> d < 0 \<and> e \<le> 0"
   238   using ball_eq_cball_iff by blast
   239 
   240 lemma finite_ball_avoid:
   241   fixes S :: "'a :: euclidean_space set"
   242   assumes "open S" "finite X" "p \<in> S"
   243   shows "\<exists>e>0. \<forall>w\<in>ball p e. w\<in>S \<and> (w\<noteq>p \<longrightarrow> w\<notin>X)"
   244 proof -
   245   obtain e1 where "0 < e1" and e1_b:"ball p e1 \<subseteq> S"
   246     using open_contains_ball_eq[OF \<open>open S\<close>] assms by auto
   247   obtain e2 where "0 < e2" and "\<forall>x\<in>X. x \<noteq> p \<longrightarrow> e2 \<le> dist p x"
   248     using finite_set_avoid[OF \<open>finite X\<close>,of p] by auto
   249   hence "\<forall>w\<in>ball p (min e1 e2). w\<in>S \<and> (w\<noteq>p \<longrightarrow> w\<notin>X)" using e1_b by auto
   250   thus "\<exists>e>0. \<forall>w\<in>ball p e. w \<in> S \<and> (w \<noteq> p \<longrightarrow> w \<notin> X)" using \<open>e2>0\<close> \<open>e1>0\<close>
   251     apply (rule_tac x="min e1 e2" in exI)
   252     by auto
   253 qed
   254 
   255 lemma finite_cball_avoid:
   256   fixes S :: "'a :: euclidean_space set"
   257   assumes "open S" "finite X" "p \<in> S"
   258   shows "\<exists>e>0. \<forall>w\<in>cball p e. w\<in>S \<and> (w\<noteq>p \<longrightarrow> w\<notin>X)"
   259 proof -
   260   obtain e1 where "e1>0" and e1: "\<forall>w\<in>ball p e1. w\<in>S \<and> (w\<noteq>p \<longrightarrow> w\<notin>X)"
   261     using finite_ball_avoid[OF assms] by auto
   262   define e2 where "e2 \<equiv> e1/2"
   263   have "e2>0" and "e2 < e1" unfolding e2_def using \<open>e1>0\<close> by auto
   264   then have "cball p e2 \<subseteq> ball p e1" by (subst cball_subset_ball_iff,auto)
   265   then show "\<exists>e>0. \<forall>w\<in>cball p e. w \<in> S \<and> (w \<noteq> p \<longrightarrow> w \<notin> X)" using \<open>e2>0\<close> e1 by auto
   266 qed
   267 
   268 lemma dim_cball:
   269   assumes "e > 0"
   270   shows "dim (cball (0 :: 'n::euclidean_space) e) = DIM('n)"
   271 proof -
   272   {
   273     fix x :: "'n::euclidean_space"
   274     define y where "y = (e / norm x) *\<^sub>R x"
   275     then have "y \<in> cball 0 e"
   276       using assms by auto
   277     moreover have *: "x = (norm x / e) *\<^sub>R y"
   278       using y_def assms by simp
   279     moreover from * have "x = (norm x/e) *\<^sub>R y"
   280       by auto
   281     ultimately have "x \<in> span (cball 0 e)"
   282       using span_scale[of y "cball 0 e" "norm x/e"]
   283         span_superset[of "cball 0 e"]
   284       by (simp add: span_base)
   285   }
   286   then have "span (cball 0 e) = (UNIV :: 'n::euclidean_space set)"
   287     by auto
   288   then show ?thesis
   289     using dim_span[of "cball (0 :: 'n::euclidean_space) e"] by (auto simp: dim_UNIV)
   290 qed
   291 
   292 
   293 subsection \<open>Boxes\<close>
   294 
   295 abbreviation One :: "'a::euclidean_space"
   296   where "One \<equiv> \<Sum>Basis"
   297 
   298 lemma One_non_0: assumes "One = (0::'a::euclidean_space)" shows False
   299 proof -
   300   have "dependent (Basis :: 'a set)"
   301     apply (simp add: dependent_finite)
   302     apply (rule_tac x="\<lambda>i. 1" in exI)
   303     using SOME_Basis apply (auto simp: assms)
   304     done
   305   with independent_Basis show False by force
   306 qed
   307 
   308 corollary One_neq_0[iff]: "One \<noteq> 0"
   309   by (metis One_non_0)
   310 
   311 corollary Zero_neq_One[iff]: "0 \<noteq> One"
   312   by (metis One_non_0)
   313 
   314 definition%important (in euclidean_space) eucl_less (infix "<e" 50)
   315   where "eucl_less a b \<longleftrightarrow> (\<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i)"
   316 
   317 definition%important box_eucl_less: "box a b = {x. a <e x \<and> x <e b}"
   318 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}"
   319 
   320 lemma box_def: "box a b = {x. \<forall>i\<in>Basis. a \<bullet> i < x \<bullet> i \<and> x \<bullet> i < b \<bullet> i}"
   321   and in_box_eucl_less: "x \<in> box a b \<longleftrightarrow> a <e x \<and> x <e b"
   322   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)"
   323     "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)"
   324   by (auto simp: box_eucl_less eucl_less_def cbox_def)
   325 
   326 lemma cbox_Pair_eq: "cbox (a, c) (b, d) = cbox a b \<times> cbox c d"
   327   by (force simp: cbox_def Basis_prod_def)
   328 
   329 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"
   330   by (force simp: cbox_Pair_eq)
   331 
   332 lemma cbox_Complex_eq: "cbox (Complex a c) (Complex b d) = (\<lambda>(x,y). Complex x y) ` (cbox a b \<times> cbox c d)"
   333   apply (auto simp: cbox_def Basis_complex_def)
   334   apply (rule_tac x = "(Re x, Im x)" in image_eqI)
   335   using complex_eq by auto
   336 
   337 lemma cbox_Pair_eq_0: "cbox (a, c) (b, d) = {} \<longleftrightarrow> cbox a b = {} \<or> cbox c d = {}"
   338   by (force simp: cbox_Pair_eq)
   339 
   340 lemma swap_cbox_Pair [simp]: "prod.swap ` cbox (c, a) (d, b) = cbox (a,c) (b,d)"
   341   by auto
   342 
   343 lemma mem_box_real[simp]:
   344   "(x::real) \<in> box a b \<longleftrightarrow> a < x \<and> x < b"
   345   "(x::real) \<in> cbox a b \<longleftrightarrow> a \<le> x \<and> x \<le> b"
   346   by (auto simp: mem_box)
   347 
   348 lemma box_real[simp]:
   349   fixes a b:: real
   350   shows "box a b = {a <..< b}" "cbox a b = {a .. b}"
   351   by auto
   352 
   353 lemma box_Int_box:
   354   fixes a :: "'a::euclidean_space"
   355   shows "box a b \<inter> box c d =
   356     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)"
   357   unfolding set_eq_iff and Int_iff and mem_box by auto
   358 
   359 lemma rational_boxes:
   360   fixes x :: "'a::euclidean_space"
   361   assumes "e > 0"
   362   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"
   363 proof -
   364   define e' where "e' = e / (2 * sqrt (real (DIM ('a))))"
   365   then have e: "e' > 0"
   366     using assms by (auto simp: DIM_positive)
   367   have "\<forall>i. \<exists>y. y \<in> \<rat> \<and> y < x \<bullet> i \<and> x \<bullet> i - y < e'" (is "\<forall>i. ?th i")
   368   proof
   369     fix i
   370     from Rats_dense_in_real[of "x \<bullet> i - e'" "x \<bullet> i"] e
   371     show "?th i" by auto
   372   qed
   373   from choice[OF this] obtain a where
   374     a: "\<forall>xa. a xa \<in> \<rat> \<and> a xa < x \<bullet> xa \<and> x \<bullet> xa - a xa < e'" ..
   375   have "\<forall>i. \<exists>y. y \<in> \<rat> \<and> x \<bullet> i < y \<and> y - x \<bullet> i < e'" (is "\<forall>i. ?th i")
   376   proof
   377     fix i
   378     from Rats_dense_in_real[of "x \<bullet> i" "x \<bullet> i + e'"] e
   379     show "?th i" by auto
   380   qed
   381   from choice[OF this] obtain b where
   382     b: "\<forall>xa. b xa \<in> \<rat> \<and> x \<bullet> xa < b xa \<and> b xa - x \<bullet> xa < e'" ..
   383   let ?a = "\<Sum>i\<in>Basis. a i *\<^sub>R i" and ?b = "\<Sum>i\<in>Basis. b i *\<^sub>R i"
   384   show ?thesis
   385   proof (rule exI[of _ ?a], rule exI[of _ ?b], safe)
   386     fix y :: 'a
   387     assume *: "y \<in> box ?a ?b"
   388     have "dist x y = sqrt (\<Sum>i\<in>Basis. (dist (x \<bullet> i) (y \<bullet> i))\<^sup>2)"
   389       unfolding L2_set_def[symmetric] by (rule euclidean_dist_l2)
   390     also have "\<dots> < sqrt (\<Sum>(i::'a)\<in>Basis. e^2 / real (DIM('a)))"
   391     proof (rule real_sqrt_less_mono, rule sum_strict_mono)
   392       fix i :: "'a"
   393       assume i: "i \<in> Basis"
   394       have "a i < y\<bullet>i \<and> y\<bullet>i < b i"
   395         using * i by (auto simp: box_def)
   396       moreover have "a i < x\<bullet>i" "x\<bullet>i - a i < e'"
   397         using a by auto
   398       moreover have "x\<bullet>i < b i" "b i - x\<bullet>i < e'"
   399         using b by auto
   400       ultimately have "\<bar>x\<bullet>i - y\<bullet>i\<bar> < 2 * e'"
   401         by auto
   402       then have "dist (x \<bullet> i) (y \<bullet> i) < e/sqrt (real (DIM('a)))"
   403         unfolding e'_def by (auto simp: dist_real_def)
   404       then have "(dist (x \<bullet> i) (y \<bullet> i))\<^sup>2 < (e/sqrt (real (DIM('a))))\<^sup>2"
   405         by (rule power_strict_mono) auto
   406       then show "(dist (x \<bullet> i) (y \<bullet> i))\<^sup>2 < e\<^sup>2 / real DIM('a)"
   407         by (simp add: power_divide)
   408     qed auto
   409     also have "\<dots> = e"
   410       using \<open>0 < e\<close> by simp
   411     finally show "y \<in> ball x e"
   412       by (auto simp: ball_def)
   413   qed (insert a b, auto simp: box_def)
   414 qed
   415 
   416 lemma open_UNION_box:
   417   fixes M :: "'a::euclidean_space set"
   418   assumes "open M"
   419   defines "a' \<equiv> \<lambda>f :: 'a \<Rightarrow> real \<times> real. (\<Sum>(i::'a)\<in>Basis. fst (f i) *\<^sub>R i)"
   420   defines "b' \<equiv> \<lambda>f :: 'a \<Rightarrow> real \<times> real. (\<Sum>(i::'a)\<in>Basis. snd (f i) *\<^sub>R i)"
   421   defines "I \<equiv> {f\<in>Basis \<rightarrow>\<^sub>E \<rat> \<times> \<rat>. box (a' f) (b' f) \<subseteq> M}"
   422   shows "M = (\<Union>f\<in>I. box (a' f) (b' f))"
   423 proof -
   424   have "x \<in> (\<Union>f\<in>I. box (a' f) (b' f))" if "x \<in> M" for x
   425   proof -
   426     obtain e where e: "e > 0" "ball x e \<subseteq> M"
   427       using openE[OF \<open>open M\<close> \<open>x \<in> M\<close>] by auto
   428     moreover obtain a b where ab:
   429       "x \<in> box a b"
   430       "\<forall>i \<in> Basis. a \<bullet> i \<in> \<rat>"
   431       "\<forall>i\<in>Basis. b \<bullet> i \<in> \<rat>"
   432       "box a b \<subseteq> ball x e"
   433       using rational_boxes[OF e(1)] by metis
   434     ultimately show ?thesis
   435        by (intro UN_I[of "\<lambda>i\<in>Basis. (a \<bullet> i, b \<bullet> i)"])
   436           (auto simp: euclidean_representation I_def a'_def b'_def)
   437   qed
   438   then show ?thesis by (auto simp: I_def)
   439 qed
   440 
   441 corollary open_countable_Union_open_box:
   442   fixes S :: "'a :: euclidean_space set"
   443   assumes "open S"
   444   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"
   445 proof -
   446   let ?a = "\<lambda>f. (\<Sum>(i::'a)\<in>Basis. fst (f i) *\<^sub>R i)"
   447   let ?b = "\<lambda>f. (\<Sum>(i::'a)\<in>Basis. snd (f i) *\<^sub>R i)"
   448   let ?I = "{f\<in>Basis \<rightarrow>\<^sub>E \<rat> \<times> \<rat>. box (?a f) (?b f) \<subseteq> S}"
   449   let ?\<D> = "(\<lambda>f. box (?a f) (?b f)) ` ?I"
   450   show ?thesis
   451   proof
   452     have "countable ?I"
   453       by (simp add: countable_PiE countable_rat)
   454     then show "countable ?\<D>"
   455       by blast
   456     show "\<Union>?\<D> = S"
   457       using open_UNION_box [OF assms] by metis
   458   qed auto
   459 qed
   460 
   461 lemma rational_cboxes:
   462   fixes x :: "'a::euclidean_space"
   463   assumes "e > 0"
   464   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"
   465 proof -
   466   define e' where "e' = e / (2 * sqrt (real (DIM ('a))))"
   467   then have e: "e' > 0"
   468     using assms by auto
   469   have "\<forall>i. \<exists>y. y \<in> \<rat> \<and> y < x \<bullet> i \<and> x \<bullet> i - y < e'" (is "\<forall>i. ?th i")
   470   proof
   471     fix i
   472     from Rats_dense_in_real[of "x \<bullet> i - e'" "x \<bullet> i"] e
   473     show "?th i" by auto
   474   qed
   475   from choice[OF this] obtain a where
   476     a: "\<forall>u. a u \<in> \<rat> \<and> a u < x \<bullet> u \<and> x \<bullet> u - a u < e'" ..
   477   have "\<forall>i. \<exists>y. y \<in> \<rat> \<and> x \<bullet> i < y \<and> y - x \<bullet> i < e'" (is "\<forall>i. ?th i")
   478   proof
   479     fix i
   480     from Rats_dense_in_real[of "x \<bullet> i" "x \<bullet> i + e'"] e
   481     show "?th i" by auto
   482   qed
   483   from choice[OF this] obtain b where
   484     b: "\<forall>u. b u \<in> \<rat> \<and> x \<bullet> u < b u \<and> b u - x \<bullet> u < e'" ..
   485   let ?a = "\<Sum>i\<in>Basis. a i *\<^sub>R i" and ?b = "\<Sum>i\<in>Basis. b i *\<^sub>R i"
   486   show ?thesis
   487   proof (rule exI[of _ ?a], rule exI[of _ ?b], safe)
   488     fix y :: 'a
   489     assume *: "y \<in> cbox ?a ?b"
   490     have "dist x y = sqrt (\<Sum>i\<in>Basis. (dist (x \<bullet> i) (y \<bullet> i))\<^sup>2)"
   491       unfolding L2_set_def[symmetric] by (rule euclidean_dist_l2)
   492     also have "\<dots> < sqrt (\<Sum>(i::'a)\<in>Basis. e^2 / real (DIM('a)))"
   493     proof (rule real_sqrt_less_mono, rule sum_strict_mono)
   494       fix i :: "'a"
   495       assume i: "i \<in> Basis"
   496       have "a i \<le> y\<bullet>i \<and> y\<bullet>i \<le> b i"
   497         using * i by (auto simp: cbox_def)
   498       moreover have "a i < x\<bullet>i" "x\<bullet>i - a i < e'"
   499         using a by auto
   500       moreover have "x\<bullet>i < b i" "b i - x\<bullet>i < e'"
   501         using b by auto
   502       ultimately have "\<bar>x\<bullet>i - y\<bullet>i\<bar> < 2 * e'"
   503         by auto
   504       then have "dist (x \<bullet> i) (y \<bullet> i) < e/sqrt (real (DIM('a)))"
   505         unfolding e'_def by (auto simp: dist_real_def)
   506       then have "(dist (x \<bullet> i) (y \<bullet> i))\<^sup>2 < (e/sqrt (real (DIM('a))))\<^sup>2"
   507         by (rule power_strict_mono) auto
   508       then show "(dist (x \<bullet> i) (y \<bullet> i))\<^sup>2 < e\<^sup>2 / real DIM('a)"
   509         by (simp add: power_divide)
   510     qed auto
   511     also have "\<dots> = e"
   512       using \<open>0 < e\<close> by simp
   513     finally show "y \<in> ball x e"
   514       by (auto simp: ball_def)
   515   next
   516     show "x \<in> cbox (\<Sum>i\<in>Basis. a i *\<^sub>R i) (\<Sum>i\<in>Basis. b i *\<^sub>R i)"
   517       using a b less_imp_le by (auto simp: cbox_def)
   518   qed (use a b cbox_def in auto)
   519 qed
   520 
   521 lemma open_UNION_cbox:
   522   fixes M :: "'a::euclidean_space set"
   523   assumes "open M"
   524   defines "a' \<equiv> \<lambda>f. (\<Sum>(i::'a)\<in>Basis. fst (f i) *\<^sub>R i)"
   525   defines "b' \<equiv> \<lambda>f. (\<Sum>(i::'a)\<in>Basis. snd (f i) *\<^sub>R i)"
   526   defines "I \<equiv> {f\<in>Basis \<rightarrow>\<^sub>E \<rat> \<times> \<rat>. cbox (a' f) (b' f) \<subseteq> M}"
   527   shows "M = (\<Union>f\<in>I. cbox (a' f) (b' f))"
   528 proof -
   529   have "x \<in> (\<Union>f\<in>I. cbox (a' f) (b' f))" if "x \<in> M" for x
   530   proof -
   531     obtain e where e: "e > 0" "ball x e \<subseteq> M"
   532       using openE[OF \<open>open M\<close> \<open>x \<in> M\<close>] by auto
   533     moreover obtain a b where ab: "x \<in> cbox a b" "\<forall>i \<in> Basis. a \<bullet> i \<in> \<rat>"
   534                                   "\<forall>i \<in> Basis. b \<bullet> i \<in> \<rat>" "cbox a b \<subseteq> ball x e"
   535       using rational_cboxes[OF e(1)] by metis
   536     ultimately show ?thesis
   537        by (intro UN_I[of "\<lambda>i\<in>Basis. (a \<bullet> i, b \<bullet> i)"])
   538           (auto simp: euclidean_representation I_def a'_def b'_def)
   539   qed
   540   then show ?thesis by (auto simp: I_def)
   541 qed
   542 
   543 corollary open_countable_Union_open_cbox:
   544   fixes S :: "'a :: euclidean_space set"
   545   assumes "open S"
   546   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"
   547 proof -
   548   let ?a = "\<lambda>f. (\<Sum>(i::'a)\<in>Basis. fst (f i) *\<^sub>R i)"
   549   let ?b = "\<lambda>f. (\<Sum>(i::'a)\<in>Basis. snd (f i) *\<^sub>R i)"
   550   let ?I = "{f\<in>Basis \<rightarrow>\<^sub>E \<rat> \<times> \<rat>. cbox (?a f) (?b f) \<subseteq> S}"
   551   let ?\<D> = "(\<lambda>f. cbox (?a f) (?b f)) ` ?I"
   552   show ?thesis
   553   proof
   554     have "countable ?I"
   555       by (simp add: countable_PiE countable_rat)
   556     then show "countable ?\<D>"
   557       by blast
   558     show "\<Union>?\<D> = S"
   559       using open_UNION_cbox [OF assms] by metis
   560   qed auto
   561 qed
   562 
   563 lemma box_eq_empty:
   564   fixes a :: "'a::euclidean_space"
   565   shows "(box a b = {} \<longleftrightarrow> (\<exists>i\<in>Basis. b\<bullet>i \<le> a\<bullet>i))" (is ?th1)
   566     and "(cbox a b = {} \<longleftrightarrow> (\<exists>i\<in>Basis. b\<bullet>i < a\<bullet>i))" (is ?th2)
   567 proof -
   568   {
   569     fix i x
   570     assume i: "i\<in>Basis" and as:"b\<bullet>i \<le> a\<bullet>i" and x:"x\<in>box a b"
   571     then have "a \<bullet> i < x \<bullet> i \<and> x \<bullet> i < b \<bullet> i"
   572       unfolding mem_box by (auto simp: box_def)
   573     then have "a\<bullet>i < b\<bullet>i" by auto
   574     then have False using as by auto
   575   }
   576   moreover
   577   {
   578     assume as: "\<forall>i\<in>Basis. \<not> (b\<bullet>i \<le> a\<bullet>i)"
   579     let ?x = "(1/2) *\<^sub>R (a + b)"
   580     {
   581       fix i :: 'a
   582       assume i: "i \<in> Basis"
   583       have "a\<bullet>i < b\<bullet>i"
   584         using as[THEN bspec[where x=i]] i by auto
   585       then have "a\<bullet>i < ((1/2) *\<^sub>R (a+b)) \<bullet> i" "((1/2) *\<^sub>R (a+b)) \<bullet> i < b\<bullet>i"
   586         by (auto simp: inner_add_left)
   587     }
   588     then have "box a b \<noteq> {}"
   589       using mem_box(1)[of "?x" a b] by auto
   590   }
   591   ultimately show ?th1 by blast
   592 
   593   {
   594     fix i x
   595     assume i: "i \<in> Basis" and as:"b\<bullet>i < a\<bullet>i" and x:"x\<in>cbox a b"
   596     then have "a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i"
   597       unfolding mem_box by auto
   598     then have "a\<bullet>i \<le> b\<bullet>i" by auto
   599     then have False using as by auto
   600   }
   601   moreover
   602   {
   603     assume as:"\<forall>i\<in>Basis. \<not> (b\<bullet>i < a\<bullet>i)"
   604     let ?x = "(1/2) *\<^sub>R (a + b)"
   605     {
   606       fix i :: 'a
   607       assume i:"i \<in> Basis"
   608       have "a\<bullet>i \<le> b\<bullet>i"
   609         using as[THEN bspec[where x=i]] i by auto
   610       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"
   611         by (auto simp: inner_add_left)
   612     }
   613     then have "cbox a b \<noteq> {}"
   614       using mem_box(2)[of "?x" a b] by auto
   615   }
   616   ultimately show ?th2 by blast
   617 qed
   618 
   619 lemma box_ne_empty:
   620   fixes a :: "'a::euclidean_space"
   621   shows "cbox a b \<noteq> {} \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i)"
   622   and "box a b \<noteq> {} \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i)"
   623   unfolding box_eq_empty[of a b] by fastforce+
   624 
   625 lemma
   626   fixes a :: "'a::euclidean_space"
   627   shows cbox_sing [simp]: "cbox a a = {a}"
   628     and box_sing [simp]: "box a a = {}"
   629   unfolding set_eq_iff mem_box eq_iff [symmetric]
   630   by (auto intro!: euclidean_eqI[where 'a='a])
   631      (metis all_not_in_conv nonempty_Basis)
   632 
   633 lemma subset_box_imp:
   634   fixes a :: "'a::euclidean_space"
   635   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"
   636     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"
   637     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"
   638      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"
   639   unfolding subset_eq[unfolded Ball_def] unfolding mem_box
   640   by (best intro: order_trans less_le_trans le_less_trans less_imp_le)+
   641 
   642 lemma box_subset_cbox:
   643   fixes a :: "'a::euclidean_space"
   644   shows "box a b \<subseteq> cbox a b"
   645   unfolding subset_eq [unfolded Ball_def] mem_box
   646   by (fast intro: less_imp_le)
   647 
   648 lemma subset_box:
   649   fixes a :: "'a::euclidean_space"
   650   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)
   651     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)
   652     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)
   653     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)
   654 proof -
   655   let ?lesscd = "\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i"
   656   let ?lerhs = "\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i"
   657   show ?th1 ?th2
   658     by (fastforce simp: mem_box)+
   659   have acdb: "a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i"
   660     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
   661   proof -
   662     have "box c d \<noteq> {}"
   663       using that
   664       unfolding box_eq_empty by force
   665     { 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"
   666       assume *: "a\<bullet>i > c\<bullet>i"
   667       then have "c \<bullet> j < ?x \<bullet> j \<and> ?x \<bullet> j < d \<bullet> j" if "j \<in> Basis" for j
   668         using cd that by (fastforce simp add: i *)
   669       then have "?x \<in> box c d"
   670         unfolding mem_box by auto
   671       moreover have "?x \<notin> cbox a b"
   672         using i cd * by (force simp: mem_box)
   673       ultimately have False using box by auto
   674     }
   675     then have "a\<bullet>i \<le> c\<bullet>i" by force
   676     moreover
   677     { 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"
   678       assume *: "b\<bullet>i < d\<bullet>i"
   679       then have "d \<bullet> j > ?x \<bullet> j \<and> ?x \<bullet> j > c \<bullet> j" if "j \<in> Basis" for j
   680         using cd that by (fastforce simp add: i *)
   681       then have "?x \<in> box c d"
   682         unfolding mem_box by auto
   683       moreover have "?x \<notin> cbox a b"
   684         using i cd * by (force simp: mem_box)
   685       ultimately have False using box by auto
   686     }
   687     then have "b\<bullet>i \<ge> d\<bullet>i" by (rule ccontr) auto
   688     ultimately show ?thesis by auto
   689   qed
   690   show ?th3
   691     using acdb by (fastforce simp add: mem_box)
   692   have acdb': "a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i"
   693     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
   694       using box_subset_cbox[of a b] that acdb by auto
   695   show ?th4
   696     using acdb' by (fastforce simp add: mem_box)
   697 qed
   698 
   699 lemma eq_cbox: "cbox a b = cbox c d \<longleftrightarrow> cbox a b = {} \<and> cbox c d = {} \<or> a = c \<and> b = d"
   700       (is "?lhs = ?rhs")
   701 proof
   702   assume ?lhs
   703   then have "cbox a b \<subseteq> cbox c d" "cbox c d \<subseteq> cbox a b"
   704     by auto
   705   then show ?rhs
   706     by (force simp: subset_box box_eq_empty intro: antisym euclidean_eqI)
   707 next
   708   assume ?rhs
   709   then show ?lhs
   710     by force
   711 qed
   712 
   713 lemma eq_cbox_box [simp]: "cbox a b = box c d \<longleftrightarrow> cbox a b = {} \<and> box c d = {}"
   714   (is "?lhs \<longleftrightarrow> ?rhs")
   715 proof
   716   assume L: ?lhs
   717   then have "cbox a b \<subseteq> box c d" "box c d \<subseteq> cbox a b"
   718     by auto
   719   then show ?rhs
   720     apply (simp add: subset_box)
   721     using L box_ne_empty box_sing apply (fastforce simp add:)
   722     done
   723 qed force
   724 
   725 lemma eq_box_cbox [simp]: "box a b = cbox c d \<longleftrightarrow> box a b = {} \<and> cbox c d = {}"
   726   by (metis eq_cbox_box)
   727 
   728 lemma eq_box: "box a b = box c d \<longleftrightarrow> box a b = {} \<and> box c d = {} \<or> a = c \<and> b = d"
   729   (is "?lhs \<longleftrightarrow> ?rhs")
   730 proof
   731   assume L: ?lhs
   732   then have "box a b \<subseteq> box c d" "box c d \<subseteq> box a b"
   733     by auto
   734   then show ?rhs
   735     apply (simp add: subset_box)
   736     using box_ne_empty(2) L
   737     apply auto
   738      apply (meson euclidean_eqI less_eq_real_def not_less)+
   739     done
   740 qed force
   741 
   742 lemma subset_box_complex:
   743    "cbox a b \<subseteq> cbox c d \<longleftrightarrow>
   744       (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"
   745    "cbox a b \<subseteq> box c d \<longleftrightarrow>
   746       (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"
   747    "box a b \<subseteq> cbox c d \<longleftrightarrow>
   748       (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"
   749    "box a b \<subseteq> box c d \<longleftrightarrow>
   750       (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"
   751   by (subst subset_box; force simp: Basis_complex_def)+
   752 
   753 lemma Int_interval:
   754   fixes a :: "'a::euclidean_space"
   755   shows "cbox a b \<inter> cbox c d =
   756     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)"
   757   unfolding set_eq_iff and Int_iff and mem_box
   758   by auto
   759 
   760 lemma disjoint_interval:
   761   fixes a::"'a::euclidean_space"
   762   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)
   763     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)
   764     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)
   765     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)
   766 proof -
   767   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"
   768   have **: "\<And>P Q. (\<And>i :: 'a. i \<in> Basis \<Longrightarrow> Q ?z i \<Longrightarrow> P i) \<Longrightarrow>
   769       (\<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)"
   770     by blast
   771   note * = set_eq_iff Int_iff empty_iff mem_box ball_conj_distrib[symmetric] eq_False ball_simps(10)
   772   show ?th1 unfolding * by (intro **) auto
   773   show ?th2 unfolding * by (intro **) auto
   774   show ?th3 unfolding * by (intro **) auto
   775   show ?th4 unfolding * by (intro **) auto
   776 qed
   777 
   778 lemma UN_box_eq_UNIV: "(\<Union>i::nat. box (- (real i *\<^sub>R One)) (real i *\<^sub>R One)) = UNIV"
   779 proof -
   780   have "\<bar>x \<bullet> b\<bar> < real_of_int (\<lceil>Max ((\<lambda>b. \<bar>x \<bullet> b\<bar>)`Basis)\<rceil> + 1)"
   781     if [simp]: "b \<in> Basis" for x b :: 'a
   782   proof -
   783     have "\<bar>x \<bullet> b\<bar> \<le> real_of_int \<lceil>\<bar>x \<bullet> b\<bar>\<rceil>"
   784       by (rule le_of_int_ceiling)
   785     also have "\<dots> \<le> real_of_int \<lceil>Max ((\<lambda>b. \<bar>x \<bullet> b\<bar>)`Basis)\<rceil>"
   786       by (auto intro!: ceiling_mono)
   787     also have "\<dots> < real_of_int (\<lceil>Max ((\<lambda>b. \<bar>x \<bullet> b\<bar>)`Basis)\<rceil> + 1)"
   788       by simp
   789     finally show ?thesis .
   790   qed
   791   then have "\<exists>n::nat. \<forall>b\<in>Basis. \<bar>x \<bullet> b\<bar> < real n" for x :: 'a
   792     by (metis order.strict_trans reals_Archimedean2)
   793   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"
   794     by auto
   795   ultimately show ?thesis
   796     by (auto simp: box_def inner_sum_left inner_Basis sum.If_cases)
   797 qed
   798 
   799 lemma image_affinity_cbox: fixes m::real
   800   fixes a b c :: "'a::euclidean_space"
   801   shows "(\<lambda>x. m *\<^sub>R x + c) ` cbox a b =
   802     (if cbox a b = {} then {}
   803      else (if 0 \<le> m then cbox (m *\<^sub>R a + c) (m *\<^sub>R b + c)
   804      else cbox (m *\<^sub>R b + c) (m *\<^sub>R a + c)))"
   805 proof (cases "m = 0")
   806   case True
   807   {
   808     fix x
   809     assume "\<forall>i\<in>Basis. x \<bullet> i \<le> c \<bullet> i" "\<forall>i\<in>Basis. c \<bullet> i \<le> x \<bullet> i"
   810     then have "x = c"
   811       by (simp add: dual_order.antisym euclidean_eqI)
   812   }
   813   moreover have "c \<in> cbox (m *\<^sub>R a + c) (m *\<^sub>R b + c)"
   814     unfolding True by (auto simp: cbox_sing)
   815   ultimately show ?thesis using True by (auto simp: cbox_def)
   816 next
   817   case False
   818   {
   819     fix y
   820     assume "\<forall>i\<in>Basis. a \<bullet> i \<le> y \<bullet> i" "\<forall>i\<in>Basis. y \<bullet> i \<le> b \<bullet> i" "m > 0"
   821     then have "\<forall>i\<in>Basis. (m *\<^sub>R a + c) \<bullet> i \<le> (m *\<^sub>R y + c) \<bullet> i" and "\<forall>i\<in>Basis. (m *\<^sub>R y + c) \<bullet> i \<le> (m *\<^sub>R b + c) \<bullet> i"
   822       by (auto simp: inner_distrib)
   823   }
   824   moreover
   825   {
   826     fix y
   827     assume "\<forall>i\<in>Basis. a \<bullet> i \<le> y \<bullet> i" "\<forall>i\<in>Basis. y \<bullet> i \<le> b \<bullet> i" "m < 0"
   828     then have "\<forall>i\<in>Basis. (m *\<^sub>R b + c) \<bullet> i \<le> (m *\<^sub>R y + c) \<bullet> i" and "\<forall>i\<in>Basis. (m *\<^sub>R y + c) \<bullet> i \<le> (m *\<^sub>R a + c) \<bullet> i"
   829       by (auto simp: mult_left_mono_neg inner_distrib)
   830   }
   831   moreover
   832   {
   833     fix y
   834     assume "m > 0" and "\<forall>i\<in>Basis. (m *\<^sub>R a + c) \<bullet> i \<le> y \<bullet> i" and "\<forall>i\<in>Basis. y \<bullet> i \<le> (m *\<^sub>R b + c) \<bullet> i"
   835     then have "y \<in> (\<lambda>x. m *\<^sub>R x + c) ` cbox a b"
   836       unfolding image_iff Bex_def mem_box
   837       apply (intro exI[where x="(1 / m) *\<^sub>R (y - c)"])
   838       apply (auto simp: pos_le_divide_eq pos_divide_le_eq mult.commute inner_distrib inner_diff_left)
   839       done
   840   }
   841   moreover
   842   {
   843     fix y
   844     assume "\<forall>i\<in>Basis. (m *\<^sub>R b + c) \<bullet> i \<le> y \<bullet> i" "\<forall>i\<in>Basis. y \<bullet> i \<le> (m *\<^sub>R a + c) \<bullet> i" "m < 0"
   845     then have "y \<in> (\<lambda>x. m *\<^sub>R x + c) ` cbox a b"
   846       unfolding image_iff Bex_def mem_box
   847       apply (intro exI[where x="(1 / m) *\<^sub>R (y - c)"])
   848       apply (auto simp: neg_le_divide_eq neg_divide_le_eq mult.commute inner_distrib inner_diff_left)
   849       done
   850   }
   851   ultimately show ?thesis using False by (auto simp: cbox_def)
   852 qed
   853 
   854 lemma image_smult_cbox:"(\<lambda>x. m *\<^sub>R (x::_::euclidean_space)) ` cbox a b =
   855   (if cbox a b = {} then {} else if 0 \<le> m then cbox (m *\<^sub>R a) (m *\<^sub>R b) else cbox (m *\<^sub>R b) (m *\<^sub>R a))"
   856   using image_affinity_cbox[of m 0 a b] by auto
   857 
   858 lemma swap_continuous:
   859   assumes "continuous_on (cbox (a,c) (b,d)) (\<lambda>(x,y). f x y)"
   860     shows "continuous_on (cbox (c,a) (d,b)) (\<lambda>(x, y). f y x)"
   861 proof -
   862   have "(\<lambda>(x, y). f y x) = (\<lambda>(x, y). f x y) \<circ> prod.swap"
   863     by auto
   864   then show ?thesis
   865     apply (rule ssubst)
   866     apply (rule continuous_on_compose)
   867     apply (simp add: split_def)
   868     apply (rule continuous_intros | simp add: assms)+
   869     done
   870 qed
   871 
   872 
   873 subsection \<open>General Intervals\<close>
   874 
   875 definition%important "is_interval (s::('a::euclidean_space) set) \<longleftrightarrow>
   876   (\<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)"
   877 
   878 lemma is_interval_1:
   879   "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)"
   880   unfolding is_interval_def by auto
   881 
   882 lemma is_interval_inter: "is_interval X \<Longrightarrow> is_interval Y \<Longrightarrow> is_interval (X \<inter> Y)"
   883   unfolding is_interval_def
   884   by blast
   885 
   886 lemma is_interval_cbox [simp]: "is_interval (cbox a (b::'a::euclidean_space))" (is ?th1)
   887   and is_interval_box [simp]: "is_interval (box a b)" (is ?th2)
   888   unfolding is_interval_def mem_box Ball_def atLeastAtMost_iff
   889   by (meson order_trans le_less_trans less_le_trans less_trans)+
   890 
   891 lemma is_interval_empty [iff]: "is_interval {}"
   892   unfolding is_interval_def  by simp
   893 
   894 lemma is_interval_univ [iff]: "is_interval UNIV"
   895   unfolding is_interval_def  by simp
   896 
   897 lemma mem_is_intervalI:
   898   assumes "is_interval s"
   899     and "a \<in> s" "b \<in> s"
   900     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"
   901   shows "x \<in> s"
   902   by (rule assms(1)[simplified is_interval_def, rule_format, OF assms(2,3,4)])
   903 
   904 lemma interval_subst:
   905   fixes S::"'a::euclidean_space set"
   906   assumes "is_interval S"
   907     and "x \<in> S" "y j \<in> S"
   908     and "j \<in> Basis"
   909   shows "(\<Sum>i\<in>Basis. (if i = j then y i \<bullet> i else x \<bullet> i) *\<^sub>R i) \<in> S"
   910   by (rule mem_is_intervalI[OF assms(1,2)]) (auto simp: assms)
   911 
   912 lemma mem_box_componentwiseI:
   913   fixes S::"'a::euclidean_space set"
   914   assumes "is_interval S"
   915   assumes "\<And>i. i \<in> Basis \<Longrightarrow> x \<bullet> i \<in> ((\<lambda>x. x \<bullet> i) ` S)"
   916   shows "x \<in> S"
   917 proof -
   918   from assms have "\<forall>i \<in> Basis. \<exists>s \<in> S. x \<bullet> i = s \<bullet> i"
   919     by auto
   920   with finite_Basis obtain s and bs::"'a list"
   921     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"
   922       and bs: "set bs = Basis" "distinct bs"
   923     by (metis finite_distinct_list)
   924   from nonempty_Basis s obtain j where j: "j \<in> Basis" "s j \<in> S"
   925     by blast
   926   define y where
   927     "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))"
   928   have "x = (\<Sum>i\<in>Basis. (if i \<in> set bs then s i \<bullet> i else s j \<bullet> i) *\<^sub>R i)"
   929     using bs by (auto simp: s(1)[symmetric] euclidean_representation)
   930   also have [symmetric]: "y bs = \<dots>"
   931     using bs(2) bs(1)[THEN equalityD1]
   932     by (induct bs) (auto simp: y_def euclidean_representation intro!: euclidean_eqI[where 'a='a])
   933   also have "y bs \<in> S"
   934     using bs(1)[THEN equalityD1]
   935     apply (induct bs)
   936      apply (auto simp: y_def j)
   937     apply (rule interval_subst[OF assms(1)])
   938       apply (auto simp: s)
   939     done
   940   finally show ?thesis .
   941 qed
   942 
   943 lemma cbox01_nonempty [simp]: "cbox 0 One \<noteq> {}"
   944   by (simp add: box_ne_empty inner_Basis inner_sum_left sum_nonneg)
   945 
   946 lemma box01_nonempty [simp]: "box 0 One \<noteq> {}"
   947   by (simp add: box_ne_empty inner_Basis inner_sum_left)
   948 
   949 lemma empty_as_interval: "{} = cbox One (0::'a::euclidean_space)"
   950   using nonempty_Basis box01_nonempty box_eq_empty(1) box_ne_empty(1) by blast
   951 
   952 lemma interval_subset_is_interval:
   953   assumes "is_interval S"
   954   shows "cbox a b \<subseteq> S \<longleftrightarrow> cbox a b = {} \<or> a \<in> S \<and> b \<in> S" (is "?lhs = ?rhs")
   955 proof
   956   assume ?lhs
   957   then show ?rhs  using box_ne_empty(1) mem_box(2) by fastforce
   958 next
   959   assume ?rhs
   960   have "cbox a b \<subseteq> S" if "a \<in> S" "b \<in> S"
   961     using assms unfolding is_interval_def
   962     apply (clarsimp simp add: mem_box)
   963     using that by blast
   964   with \<open>?rhs\<close> show ?lhs
   965     by blast
   966 qed
   967 
   968 lemma is_real_interval_union:
   969   "is_interval (X \<union> Y)"
   970   if X: "is_interval X" and Y: "is_interval Y" and I: "(X \<noteq> {} \<Longrightarrow> Y \<noteq> {} \<Longrightarrow> X \<inter> Y \<noteq> {})"
   971   for X Y::"real set"
   972 proof -
   973   consider "X \<noteq> {}" "Y \<noteq> {}" | "X = {}" | "Y = {}" by blast
   974   then show ?thesis
   975   proof cases
   976     case 1
   977     then obtain r where "r \<in> X \<or> X \<inter> Y = {}" "r \<in> Y \<or> X \<inter> Y = {}"
   978       by blast
   979     then show ?thesis
   980       using I 1 X Y unfolding is_interval_1
   981       by (metis (full_types) Un_iff le_cases)
   982   qed (use that in auto)
   983 qed
   984 
   985 lemma is_interval_translationI:
   986   assumes "is_interval X"
   987   shows "is_interval ((+) x ` X)"
   988   unfolding is_interval_def
   989 proof safe
   990   fix b d e
   991   assume "b \<in> X" "d \<in> X"
   992     "\<forall>i\<in>Basis. (x + b) \<bullet> i \<le> e \<bullet> i \<and> e \<bullet> i \<le> (x + d) \<bullet> i \<or>
   993        (x + d) \<bullet> i \<le> e \<bullet> i \<and> e \<bullet> i \<le> (x + b) \<bullet> i"
   994   hence "e - x \<in> X"
   995     by (intro mem_is_intervalI[OF assms \<open>b \<in> X\<close> \<open>d \<in> X\<close>, of "e - x"])
   996       (auto simp: algebra_simps)
   997   thus "e \<in> (+) x ` X" by force
   998 qed
   999 
  1000 lemma is_interval_uminusI:
  1001   assumes "is_interval X"
  1002   shows "is_interval (uminus ` X)"
  1003   unfolding is_interval_def
  1004 proof safe
  1005   fix b d e
  1006   assume "b \<in> X" "d \<in> X"
  1007     "\<forall>i\<in>Basis. (- b) \<bullet> i \<le> e \<bullet> i \<and> e \<bullet> i \<le> (- d) \<bullet> i \<or>
  1008        (- d) \<bullet> i \<le> e \<bullet> i \<and> e \<bullet> i \<le> (- b) \<bullet> i"
  1009   hence "- e \<in> X"
  1010     by (intro mem_is_intervalI[OF assms \<open>b \<in> X\<close> \<open>d \<in> X\<close>, of "- e"])
  1011       (auto simp: algebra_simps)
  1012   thus "e \<in> uminus ` X" by force
  1013 qed
  1014 
  1015 lemma is_interval_uminus[simp]: "is_interval (uminus ` x) = is_interval x"
  1016   using is_interval_uminusI[of x] is_interval_uminusI[of "uminus ` x"]
  1017   by (auto simp: image_image)
  1018 
  1019 lemma is_interval_neg_translationI:
  1020   assumes "is_interval X"
  1021   shows "is_interval ((-) x ` X)"
  1022 proof -
  1023   have "(-) x ` X = (+) x ` uminus ` X"
  1024     by (force simp: algebra_simps)
  1025   also have "is_interval \<dots>"
  1026     by (metis is_interval_uminusI is_interval_translationI assms)
  1027   finally show ?thesis .
  1028 qed
  1029 
  1030 lemma is_interval_translation[simp]:
  1031   "is_interval ((+) x ` X) = is_interval X"
  1032   using is_interval_neg_translationI[of "(+) x ` X" x]
  1033   by (auto intro!: is_interval_translationI simp: image_image)
  1034 
  1035 lemma is_interval_minus_translation[simp]:
  1036   shows "is_interval ((-) x ` X) = is_interval X"
  1037 proof -
  1038   have "(-) x ` X = (+) x ` uminus ` X"
  1039     by (force simp: algebra_simps)
  1040   also have "is_interval \<dots> = is_interval X"
  1041     by simp
  1042   finally show ?thesis .
  1043 qed
  1044 
  1045 lemma is_interval_minus_translation'[simp]:
  1046   shows "is_interval ((\<lambda>x. x - c) ` X) = is_interval X"
  1047   using is_interval_translation[of "-c" X]
  1048   by (metis image_cong uminus_add_conv_diff)
  1049 
  1050 
  1051 subsection%unimportant \<open>Bounded Projections\<close>
  1052 
  1053 lemma bounded_inner_imp_bdd_above:
  1054   assumes "bounded s"
  1055     shows "bdd_above ((\<lambda>x. x \<bullet> a) ` s)"
  1056 by (simp add: assms bounded_imp_bdd_above bounded_linear_image bounded_linear_inner_left)
  1057 
  1058 lemma bounded_inner_imp_bdd_below:
  1059   assumes "bounded s"
  1060     shows "bdd_below ((\<lambda>x. x \<bullet> a) ` s)"
  1061 by (simp add: assms bounded_imp_bdd_below bounded_linear_image bounded_linear_inner_left)
  1062 
  1063 
  1064 subsection%unimportant \<open>Structural rules for pointwise continuity\<close>
  1065 
  1066 lemma continuous_infnorm[continuous_intros]:
  1067   "continuous F f \<Longrightarrow> continuous F (\<lambda>x. infnorm (f x))"
  1068   unfolding continuous_def by (rule tendsto_infnorm)
  1069 
  1070 lemma continuous_inner[continuous_intros]:
  1071   assumes "continuous F f"
  1072     and "continuous F g"
  1073   shows "continuous F (\<lambda>x. inner (f x) (g x))"
  1074   using assms unfolding continuous_def by (rule tendsto_inner)
  1075 
  1076 
  1077 subsection%unimportant \<open>Structural rules for setwise continuity\<close>
  1078 
  1079 lemma continuous_on_infnorm[continuous_intros]:
  1080   "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. infnorm (f x))"
  1081   unfolding continuous_on by (fast intro: tendsto_infnorm)
  1082 
  1083 lemma continuous_on_inner[continuous_intros]:
  1084   fixes g :: "'a::topological_space \<Rightarrow> 'b::real_inner"
  1085   assumes "continuous_on s f"
  1086     and "continuous_on s g"
  1087   shows "continuous_on s (\<lambda>x. inner (f x) (g x))"
  1088   using bounded_bilinear_inner assms
  1089   by (rule bounded_bilinear.continuous_on)
  1090 
  1091 
  1092 subsection%unimportant \<open>Openness of halfspaces.\<close>
  1093 
  1094 lemma open_halfspace_lt: "open {x. inner a x < b}"
  1095   by (simp add: open_Collect_less continuous_on_inner continuous_on_const continuous_on_id)
  1096 
  1097 lemma open_halfspace_gt: "open {x. inner a x > b}"
  1098   by (simp add: open_Collect_less continuous_on_inner continuous_on_const continuous_on_id)
  1099 
  1100 lemma open_halfspace_component_lt: "open {x::'a::euclidean_space. x\<bullet>i < a}"
  1101   by (simp add: open_Collect_less continuous_on_inner continuous_on_const continuous_on_id)
  1102 
  1103 lemma open_halfspace_component_gt: "open {x::'a::euclidean_space. x\<bullet>i > a}"
  1104   by (simp add: open_Collect_less continuous_on_inner continuous_on_const continuous_on_id)
  1105 
  1106 lemma eucl_less_eq_halfspaces:
  1107   fixes a :: "'a::euclidean_space"
  1108   shows "{x. x <e a} = (\<Inter>i\<in>Basis. {x. x \<bullet> i < a \<bullet> i})"
  1109         "{x. a <e x} = (\<Inter>i\<in>Basis. {x. a \<bullet> i < x \<bullet> i})"
  1110   by (auto simp: eucl_less_def)
  1111 
  1112 lemma open_Collect_eucl_less[simp, intro]:
  1113   fixes a :: "'a::euclidean_space"
  1114   shows "open {x. x <e a}" "open {x. a <e x}"
  1115   by (auto simp: eucl_less_eq_halfspaces open_halfspace_component_lt open_halfspace_component_gt)
  1116 
  1117 subsection%unimportant \<open>Closure of halfspaces and hyperplanes\<close>
  1118 
  1119 lemma continuous_at_inner: "continuous (at x) (inner a)"
  1120   unfolding continuous_at by (intro tendsto_intros)
  1121 
  1122 lemma closed_halfspace_le: "closed {x. inner a x \<le> b}"
  1123   by (simp add: closed_Collect_le continuous_on_inner continuous_on_const continuous_on_id)
  1124 
  1125 lemma closed_halfspace_ge: "closed {x. inner a x \<ge> b}"
  1126   by (simp add: closed_Collect_le continuous_on_inner continuous_on_const continuous_on_id)
  1127 
  1128 lemma closed_hyperplane: "closed {x. inner a x = b}"
  1129   by (simp add: closed_Collect_eq continuous_on_inner continuous_on_const continuous_on_id)
  1130 
  1131 lemma closed_halfspace_component_le: "closed {x::'a::euclidean_space. x\<bullet>i \<le> a}"
  1132   by (simp add: closed_Collect_le continuous_on_inner continuous_on_const continuous_on_id)
  1133 
  1134 lemma closed_halfspace_component_ge: "closed {x::'a::euclidean_space. x\<bullet>i \<ge> a}"
  1135   by (simp add: closed_Collect_le continuous_on_inner continuous_on_const continuous_on_id)
  1136 
  1137 lemma closed_interval_left:
  1138   fixes b :: "'a::euclidean_space"
  1139   shows "closed {x::'a. \<forall>i\<in>Basis. x\<bullet>i \<le> b\<bullet>i}"
  1140   by (simp add: Collect_ball_eq closed_INT closed_Collect_le continuous_on_inner continuous_on_const continuous_on_id)
  1141 
  1142 lemma closed_interval_right:
  1143   fixes a :: "'a::euclidean_space"
  1144   shows "closed {x::'a. \<forall>i\<in>Basis. a\<bullet>i \<le> x\<bullet>i}"
  1145   by (simp add: Collect_ball_eq closed_INT closed_Collect_le continuous_on_inner continuous_on_const continuous_on_id)
  1146 
  1147 
  1148 subsection%unimportant\<open>Some more convenient intermediate-value theorem formulations\<close>
  1149 
  1150 lemma connected_ivt_hyperplane:
  1151   assumes "connected S" and xy: "x \<in> S" "y \<in> S" and b: "inner a x \<le> b" "b \<le> inner a y"
  1152   shows "\<exists>z \<in> S. inner a z = b"
  1153 proof (rule ccontr)
  1154   assume as:"\<not> (\<exists>z\<in>S. inner a z = b)"
  1155   let ?A = "{x. inner a x < b}"
  1156   let ?B = "{x. inner a x > b}"
  1157   have "open ?A" "open ?B"
  1158     using open_halfspace_lt and open_halfspace_gt by auto
  1159   moreover have "?A \<inter> ?B = {}" by auto
  1160   moreover have "S \<subseteq> ?A \<union> ?B" using as by auto
  1161   ultimately show False
  1162     using \<open>connected S\<close>[unfolded connected_def not_ex,
  1163       THEN spec[where x="?A"], THEN spec[where x="?B"]]
  1164     using xy b by auto
  1165 qed
  1166 
  1167 lemma connected_ivt_component:
  1168   fixes x::"'a::euclidean_space"
  1169   shows "connected S \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x\<bullet>k \<le> a \<Longrightarrow> a \<le> y\<bullet>k \<Longrightarrow> (\<exists>z\<in>S.  z\<bullet>k = a)"
  1170   using connected_ivt_hyperplane[of S x y "k::'a" a]
  1171   by (auto simp: inner_commute)
  1172 
  1173 
  1174 subsection \<open>Limit Component Bounds\<close>
  1175 
  1176 lemma Lim_component_le:
  1177   fixes f :: "'a \<Rightarrow> 'b::euclidean_space"
  1178   assumes "(f \<longlongrightarrow> l) net"
  1179     and "\<not> (trivial_limit net)"
  1180     and "eventually (\<lambda>x. f(x)\<bullet>i \<le> b) net"
  1181   shows "l\<bullet>i \<le> b"
  1182   by (rule tendsto_le[OF assms(2) tendsto_const tendsto_inner[OF assms(1) tendsto_const] assms(3)])
  1183 
  1184 lemma Lim_component_ge:
  1185   fixes f :: "'a \<Rightarrow> 'b::euclidean_space"
  1186   assumes "(f \<longlongrightarrow> l) net"
  1187     and "\<not> (trivial_limit net)"
  1188     and "eventually (\<lambda>x. b \<le> (f x)\<bullet>i) net"
  1189   shows "b \<le> l\<bullet>i"
  1190   by (rule tendsto_le[OF assms(2) tendsto_inner[OF assms(1) tendsto_const] tendsto_const assms(3)])
  1191 
  1192 lemma Lim_component_eq:
  1193   fixes f :: "'a \<Rightarrow> 'b::euclidean_space"
  1194   assumes net: "(f \<longlongrightarrow> l) net" "\<not> trivial_limit net"
  1195     and ev:"eventually (\<lambda>x. f(x)\<bullet>i = b) net"
  1196   shows "l\<bullet>i = b"
  1197   using ev[unfolded order_eq_iff eventually_conj_iff]
  1198   using Lim_component_ge[OF net, of b i]
  1199   using Lim_component_le[OF net, of i b]
  1200   by auto
  1201 
  1202 lemma open_box[intro]: "open (box a b)"
  1203 proof -
  1204   have "open (\<Inter>i\<in>Basis. ((\<bullet>) i) -` {a \<bullet> i <..< b \<bullet> i})"
  1205     by (auto intro!: continuous_open_vimage continuous_inner continuous_ident continuous_const)
  1206   also have "(\<Inter>i\<in>Basis. ((\<bullet>) i) -` {a \<bullet> i <..< b \<bullet> i}) = box a b"
  1207     by (auto simp: box_def inner_commute)
  1208   finally show ?thesis .
  1209 qed
  1210 
  1211 lemma closed_cbox[intro]:
  1212   fixes a b :: "'a::euclidean_space"
  1213   shows "closed (cbox a b)"
  1214 proof -
  1215   have "closed (\<Inter>i\<in>Basis. (\<lambda>x. x\<bullet>i) -` {a\<bullet>i .. b\<bullet>i})"
  1216     by (intro closed_INT ballI continuous_closed_vimage allI
  1217       linear_continuous_at closed_real_atLeastAtMost finite_Basis bounded_linear_inner_left)
  1218   also have "(\<Inter>i\<in>Basis. (\<lambda>x. x\<bullet>i) -` {a\<bullet>i .. b\<bullet>i}) = cbox a b"
  1219     by (auto simp: cbox_def)
  1220   finally show "closed (cbox a b)" .
  1221 qed
  1222 
  1223 lemma interior_cbox [simp]:
  1224   fixes a b :: "'a::euclidean_space"
  1225   shows "interior (cbox a b) = box a b" (is "?L = ?R")
  1226 proof(rule subset_antisym)
  1227   show "?R \<subseteq> ?L"
  1228     using box_subset_cbox open_box
  1229     by (rule interior_maximal)
  1230   {
  1231     fix x
  1232     assume "x \<in> interior (cbox a b)"
  1233     then obtain s where s: "open s" "x \<in> s" "s \<subseteq> cbox a b" ..
  1234     then obtain e where "e>0" and e:"\<forall>x'. dist x' x < e \<longrightarrow> x' \<in> cbox a b"
  1235       unfolding open_dist and subset_eq by auto
  1236     {
  1237       fix i :: 'a
  1238       assume i: "i \<in> Basis"
  1239       have "dist (x - (e / 2) *\<^sub>R i) x < e"
  1240         and "dist (x + (e / 2) *\<^sub>R i) x < e"
  1241         unfolding dist_norm
  1242         apply auto
  1243         unfolding norm_minus_cancel
  1244         using norm_Basis[OF i] \<open>e>0\<close>
  1245         apply auto
  1246         done
  1247       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"
  1248         using e[THEN spec[where x="x - (e/2) *\<^sub>R i"]]
  1249           and e[THEN spec[where x="x + (e/2) *\<^sub>R i"]]
  1250         unfolding mem_box
  1251         using i
  1252         by blast+
  1253       then have "a \<bullet> i < x \<bullet> i" and "x \<bullet> i < b \<bullet> i"
  1254         using \<open>e>0\<close> i
  1255         by (auto simp: inner_diff_left inner_Basis inner_add_left)
  1256     }
  1257     then have "x \<in> box a b"
  1258       unfolding mem_box by auto
  1259   }
  1260   then show "?L \<subseteq> ?R" ..
  1261 qed
  1262 
  1263 lemma bounded_cbox [simp]:
  1264   fixes a :: "'a::euclidean_space"
  1265   shows "bounded (cbox a b)"
  1266 proof -
  1267   let ?b = "\<Sum>i\<in>Basis. \<bar>a\<bullet>i\<bar> + \<bar>b\<bullet>i\<bar>"
  1268   {
  1269     fix x :: "'a"
  1270     assume "\<And>i. i\<in>Basis \<Longrightarrow> a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i"
  1271     then have "(\<Sum>i\<in>Basis. \<bar>x \<bullet> i\<bar>) \<le> ?b"
  1272       by (force simp: intro!: sum_mono)
  1273     then have "norm x \<le> ?b"
  1274       using norm_le_l1[of x] by auto
  1275   }
  1276   then show ?thesis
  1277     unfolding cbox_def bounded_iff by force
  1278 qed
  1279 
  1280 lemma bounded_box [simp]:
  1281   fixes a :: "'a::euclidean_space"
  1282   shows "bounded (box a b)"
  1283   using bounded_cbox[of a b] box_subset_cbox[of a b] bounded_subset[of "cbox a b" "box a b"]
  1284   by simp
  1285 
  1286 lemma not_interval_UNIV [simp]:
  1287   fixes a :: "'a::euclidean_space"
  1288   shows "cbox a b \<noteq> UNIV" "box a b \<noteq> UNIV"
  1289   using bounded_box[of a b] bounded_cbox[of a b] by force+
  1290 
  1291 lemma not_interval_UNIV2 [simp]:
  1292   fixes a :: "'a::euclidean_space"
  1293   shows "UNIV \<noteq> cbox a b" "UNIV \<noteq> box a b"
  1294   using bounded_box[of a b] bounded_cbox[of a b] by force+
  1295 
  1296 lemma box_midpoint:
  1297   fixes a :: "'a::euclidean_space"
  1298   assumes "box a b \<noteq> {}"
  1299   shows "((1/2) *\<^sub>R (a + b)) \<in> box a b"
  1300 proof -
  1301   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
  1302     using assms that by (auto simp: inner_add_left box_ne_empty)
  1303   then show ?thesis unfolding mem_box by auto
  1304 qed
  1305 
  1306 lemma open_cbox_convex:
  1307   fixes x :: "'a::euclidean_space"
  1308   assumes x: "x \<in> box a b"
  1309     and y: "y \<in> cbox a b"
  1310     and e: "0 < e" "e \<le> 1"
  1311   shows "(e *\<^sub>R x + (1 - e) *\<^sub>R y) \<in> box a b"
  1312 proof -
  1313   {
  1314     fix i :: 'a
  1315     assume i: "i \<in> Basis"
  1316     have "a \<bullet> i = e * (a \<bullet> i) + (1 - e) * (a \<bullet> i)"
  1317       unfolding left_diff_distrib by simp
  1318     also have "\<dots> < e * (x \<bullet> i) + (1 - e) * (y \<bullet> i)"
  1319     proof (rule add_less_le_mono)
  1320       show "e * (a \<bullet> i) < e * (x \<bullet> i)"
  1321         using \<open>0 < e\<close> i mem_box(1) x by auto
  1322       show "(1 - e) * (a \<bullet> i) \<le> (1 - e) * (y \<bullet> i)"
  1323         by (meson diff_ge_0_iff_ge \<open>e \<le> 1\<close> i mem_box(2) mult_left_mono y)
  1324     qed
  1325     finally have "a \<bullet> i < (e *\<^sub>R x + (1 - e) *\<^sub>R y) \<bullet> i"
  1326       unfolding inner_simps by auto
  1327     moreover
  1328     {
  1329       have "b \<bullet> i = e * (b\<bullet>i) + (1 - e) * (b\<bullet>i)"
  1330         unfolding left_diff_distrib by simp
  1331       also have "\<dots> > e * (x \<bullet> i) + (1 - e) * (y \<bullet> i)"
  1332       proof (rule add_less_le_mono)
  1333         show "e * (x \<bullet> i) < e * (b \<bullet> i)"
  1334           using \<open>0 < e\<close> i mem_box(1) x by auto
  1335         show "(1 - e) * (y \<bullet> i) \<le> (1 - e) * (b \<bullet> i)"
  1336           by (meson diff_ge_0_iff_ge \<open>e \<le> 1\<close> i mem_box(2) mult_left_mono y)
  1337       qed
  1338       finally have "(e *\<^sub>R x + (1 - e) *\<^sub>R y) \<bullet> i < b \<bullet> i"
  1339         unfolding inner_simps by auto
  1340     }
  1341     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"
  1342       by auto
  1343   }
  1344   then show ?thesis
  1345     unfolding mem_box by auto
  1346 qed
  1347 
  1348 lemma closure_cbox [simp]: "closure (cbox a b) = cbox a b"
  1349   by (simp add: closed_cbox)
  1350 
  1351 lemma closure_box [simp]:
  1352   fixes a :: "'a::euclidean_space"
  1353    assumes "box a b \<noteq> {}"
  1354   shows "closure (box a b) = cbox a b"
  1355 proof -
  1356   have ab: "a <e b"
  1357     using assms by (simp add: eucl_less_def box_ne_empty)
  1358   let ?c = "(1 / 2) *\<^sub>R (a + b)"
  1359   {
  1360     fix x
  1361     assume as:"x \<in> cbox a b"
  1362     define f where [abs_def]: "f n = x + (inverse (real n + 1)) *\<^sub>R (?c - x)" for n
  1363     {
  1364       fix n
  1365       assume fn: "f n <e b \<longrightarrow> a <e f n \<longrightarrow> f n = x" and xc: "x \<noteq> ?c"
  1366       have *: "0 < inverse (real n + 1)" "inverse (real n + 1) \<le> 1"
  1367         unfolding inverse_le_1_iff by auto
  1368       have "(inverse (real n + 1)) *\<^sub>R ((1 / 2) *\<^sub>R (a + b)) + (1 - inverse (real n + 1)) *\<^sub>R x =
  1369         x + (inverse (real n + 1)) *\<^sub>R (((1 / 2) *\<^sub>R (a + b)) - x)"
  1370         by (auto simp: algebra_simps)
  1371       then have "f n <e b" and "a <e f n"
  1372         using open_cbox_convex[OF box_midpoint[OF assms] as *]
  1373         unfolding f_def by (auto simp: box_def eucl_less_def)
  1374       then have False
  1375         using fn unfolding f_def using xc by auto
  1376     }
  1377     moreover
  1378     {
  1379       assume "\<not> (f \<longlongrightarrow> x) sequentially"
  1380       {
  1381         fix e :: real
  1382         assume "e > 0"
  1383         then obtain N :: nat where N: "inverse (real (N + 1)) < e"
  1384           using reals_Archimedean by auto
  1385         have "inverse (real n + 1) < e" if "N \<le> n" for n
  1386           by (auto intro!: that le_less_trans [OF _ N])
  1387         then have "\<exists>N::nat. \<forall>n\<ge>N. inverse (real n + 1) < e" by auto
  1388       }
  1389       then have "((\<lambda>n. inverse (real n + 1)) \<longlongrightarrow> 0) sequentially"
  1390         unfolding lim_sequentially by(auto simp: dist_norm)
  1391       then have "(f \<longlongrightarrow> x) sequentially"
  1392         unfolding f_def
  1393         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]
  1394         using tendsto_scaleR [OF _ tendsto_const, of "\<lambda>n::nat. inverse (real n + 1)" 0 sequentially "((1 / 2) *\<^sub>R (a + b) - x)"]
  1395         by auto
  1396     }
  1397     ultimately have "x \<in> closure (box a b)"
  1398       using as box_midpoint[OF assms]
  1399       unfolding closure_def islimpt_sequential
  1400       by (cases "x=?c") (auto simp: in_box_eucl_less)
  1401   }
  1402   then show ?thesis
  1403     using closure_minimal[OF box_subset_cbox, of a b] by blast
  1404 qed
  1405 
  1406 lemma bounded_subset_box_symmetric:
  1407   fixes S :: "('a::euclidean_space) set"
  1408   assumes "bounded S"
  1409   obtains a where "S \<subseteq> box (-a) a"
  1410 proof -
  1411   obtain b where "b>0" and b: "\<forall>x\<in>S. norm x \<le> b"
  1412     using assms[unfolded bounded_pos] by auto
  1413   define a :: 'a where "a = (\<Sum>i\<in>Basis. (b + 1) *\<^sub>R i)"
  1414   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
  1415     using b Basis_le_norm[OF i, of x] that by (auto simp: a_def)
  1416   then have "S \<subseteq> box (-a) a"
  1417     by (auto simp: simp add: box_def)
  1418   then show ?thesis ..
  1419 qed
  1420 
  1421 lemma bounded_subset_cbox_symmetric:
  1422   fixes S :: "('a::euclidean_space) set"
  1423   assumes "bounded S"
  1424   obtains a where "S \<subseteq> cbox (-a) a"
  1425 proof -
  1426   obtain a where "S \<subseteq> box (-a) a"
  1427     using bounded_subset_box_symmetric[OF assms] by auto
  1428   then show ?thesis
  1429     by (meson box_subset_cbox dual_order.trans that)
  1430 qed
  1431 
  1432 lemma frontier_cbox:
  1433   fixes a b :: "'a::euclidean_space"
  1434   shows "frontier (cbox a b) = cbox a b - box a b"
  1435   unfolding frontier_def unfolding interior_cbox and closure_closed[OF closed_cbox] ..
  1436 
  1437 lemma frontier_box:
  1438   fixes a b :: "'a::euclidean_space"
  1439   shows "frontier (box a b) = (if box a b = {} then {} else cbox a b - box a b)"
  1440 proof (cases "box a b = {}")
  1441   case True
  1442   then show ?thesis
  1443     using frontier_empty by auto
  1444 next
  1445   case False
  1446   then show ?thesis
  1447     unfolding frontier_def and closure_box[OF False] and interior_open[OF open_box]
  1448     by auto
  1449 qed
  1450 
  1451 lemma Int_interval_mixed_eq_empty:
  1452   fixes a :: "'a::euclidean_space"
  1453    assumes "box c d \<noteq> {}"
  1454   shows "box a b \<inter> cbox c d = {} \<longleftrightarrow> box a b \<inter> box c d = {}"
  1455   unfolding closure_box[OF assms, symmetric]
  1456   unfolding open_Int_closure_eq_empty[OF open_box] ..
  1457 
  1458 subsection \<open>Class Instances\<close>
  1459 
  1460 lemma compact_lemma:
  1461   fixes f :: "nat \<Rightarrow> 'a::euclidean_space"
  1462   assumes "bounded (range f)"
  1463   shows "\<forall>d\<subseteq>Basis. \<exists>l::'a. \<exists> r.
  1464     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)"
  1465   by (rule compact_lemma_general[where unproj="\<lambda>e. \<Sum>i\<in>Basis. e i *\<^sub>R i"])
  1466      (auto intro!: assms bounded_linear_inner_left bounded_linear_image
  1467        simp: euclidean_representation)
  1468 
  1469 instance%important euclidean_space \<subseteq> heine_borel
  1470 proof%unimportant
  1471   fix f :: "nat \<Rightarrow> 'a"
  1472   assume f: "bounded (range f)"
  1473   then obtain l::'a and r where r: "strict_mono r"
  1474     and l: "\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>Basis. dist (f (r n) \<bullet> i) (l \<bullet> i) < e) sequentially"
  1475     using compact_lemma [OF f] by blast
  1476   {
  1477     fix e::real
  1478     assume "e > 0"
  1479     hence "e / real_of_nat DIM('a) > 0" by (simp add: DIM_positive)
  1480     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"
  1481       by simp
  1482     moreover
  1483     {
  1484       fix n
  1485       assume n: "\<forall>i\<in>Basis. dist (f (r n) \<bullet> i) (l \<bullet> i) < e / (real_of_nat DIM('a))"
  1486       have "dist (f (r n)) l \<le> (\<Sum>i\<in>Basis. dist (f (r n) \<bullet> i) (l \<bullet> i))"
  1487         apply (subst euclidean_dist_l2)
  1488         using zero_le_dist
  1489         apply (rule L2_set_le_sum)
  1490         done
  1491       also have "\<dots> < (\<Sum>i\<in>(Basis::'a set). e / (real_of_nat DIM('a)))"
  1492         apply (rule sum_strict_mono)
  1493         using n
  1494         apply auto
  1495         done
  1496       finally have "dist (f (r n)) l < e"
  1497         by auto
  1498     }
  1499     ultimately have "eventually (\<lambda>n. dist (f (r n)) l < e) sequentially"
  1500       by (rule eventually_mono)
  1501   }
  1502   then have *: "((f \<circ> r) \<longlongrightarrow> l) sequentially"
  1503     unfolding o_def tendsto_iff by simp
  1504   with r show "\<exists>l r. strict_mono r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
  1505     by auto
  1506 qed
  1507 
  1508 instance%important euclidean_space \<subseteq> banach ..
  1509 
  1510 instance euclidean_space \<subseteq> second_countable_topology
  1511 proof
  1512   define a where "a f = (\<Sum>i\<in>Basis. fst (f i) *\<^sub>R i)" for f :: "'a \<Rightarrow> real \<times> real"
  1513   then have a: "\<And>f. (\<Sum>i\<in>Basis. fst (f i) *\<^sub>R i) = a f"
  1514     by simp
  1515   define b where "b f = (\<Sum>i\<in>Basis. snd (f i) *\<^sub>R i)" for f :: "'a \<Rightarrow> real \<times> real"
  1516   then have b: "\<And>f. (\<Sum>i\<in>Basis. snd (f i) *\<^sub>R i) = b f"
  1517     by simp
  1518   define B where "B = (\<lambda>f. box (a f) (b f)) ` (Basis \<rightarrow>\<^sub>E (\<rat> \<times> \<rat>))"
  1519 
  1520   have "Ball B open" by (simp add: B_def open_box)
  1521   moreover have "(\<forall>A. open A \<longrightarrow> (\<exists>B'\<subseteq>B. \<Union>B' = A))"
  1522   proof safe
  1523     fix A::"'a set"
  1524     assume "open A"
  1525     show "\<exists>B'\<subseteq>B. \<Union>B' = A"
  1526       apply (rule exI[of _ "{b\<in>B. b \<subseteq> A}"])
  1527       apply (subst (3) open_UNION_box[OF \<open>open A\<close>])
  1528       apply (auto simp: a b B_def)
  1529       done
  1530   qed
  1531   ultimately
  1532   have "topological_basis B"
  1533     unfolding topological_basis_def by blast
  1534   moreover
  1535   have "countable B"
  1536     unfolding B_def
  1537     by (intro countable_image countable_PiE finite_Basis countable_SIGMA countable_rat)
  1538   ultimately show "\<exists>B::'a set set. countable B \<and> open = generate_topology B"
  1539     by (blast intro: topological_basis_imp_subbasis)
  1540 qed
  1541 
  1542 instance euclidean_space \<subseteq> polish_space ..
  1543 
  1544 
  1545 subsection \<open>Compact Boxes\<close>
  1546 
  1547 lemma compact_cbox [simp]:
  1548   fixes a :: "'a::euclidean_space"
  1549   shows "compact (cbox a b)"
  1550   using bounded_closed_imp_seq_compact[of "cbox a b"] using bounded_cbox[of a b]
  1551   by (auto simp: compact_eq_seq_compact_metric)
  1552 
  1553 proposition is_interval_compact:
  1554    "is_interval S \<and> compact S \<longleftrightarrow> (\<exists>a b. S = cbox a b)"   (is "?lhs = ?rhs")
  1555 proof (cases "S = {}")
  1556   case True
  1557   with empty_as_interval show ?thesis by auto
  1558 next
  1559   case False
  1560   show ?thesis
  1561   proof
  1562     assume L: ?lhs
  1563     then have "is_interval S" "compact S" by auto
  1564     define a where "a \<equiv> \<Sum>i\<in>Basis. (INF x\<in>S. x \<bullet> i) *\<^sub>R i"
  1565     define b where "b \<equiv> \<Sum>i\<in>Basis. (SUP x\<in>S. x \<bullet> i) *\<^sub>R i"
  1566     have 1: "\<And>x i. \<lbrakk>x \<in> S; i \<in> Basis\<rbrakk> \<Longrightarrow> (INF x\<in>S. x \<bullet> i) \<le> x \<bullet> i"
  1567       by (simp add: cInf_lower bounded_inner_imp_bdd_below compact_imp_bounded L)
  1568     have 2: "\<And>x i. \<lbrakk>x \<in> S; i \<in> Basis\<rbrakk> \<Longrightarrow> x \<bullet> i \<le> (SUP x\<in>S. x \<bullet> i)"
  1569       by (simp add: cSup_upper bounded_inner_imp_bdd_above compact_imp_bounded L)
  1570     have 3: "x \<in> S" if inf: "\<And>i. i \<in> Basis \<Longrightarrow> (INF x\<in>S. x \<bullet> i) \<le> x \<bullet> i"
  1571                    and sup: "\<And>i. i \<in> Basis \<Longrightarrow> x \<bullet> i \<le> (SUP x\<in>S. x \<bullet> i)" for x
  1572     proof (rule mem_box_componentwiseI [OF \<open>is_interval S\<close>])
  1573       fix i::'a
  1574       assume i: "i \<in> Basis"
  1575       have cont: "continuous_on S (\<lambda>x. x \<bullet> i)"
  1576         by (intro continuous_intros)
  1577       obtain a where "a \<in> S" and a: "\<And>y. y\<in>S \<Longrightarrow> a \<bullet> i \<le> y \<bullet> i"
  1578         using continuous_attains_inf [OF \<open>compact S\<close> False cont] by blast
  1579       obtain b where "b \<in> S" and b: "\<And>y. y\<in>S \<Longrightarrow> y \<bullet> i \<le> b \<bullet> i"
  1580         using continuous_attains_sup [OF \<open>compact S\<close> False cont] by blast
  1581       have "a \<bullet> i \<le> (INF x\<in>S. x \<bullet> i)"
  1582         by (simp add: False a cINF_greatest)
  1583       also have "\<dots> \<le> x \<bullet> i"
  1584         by (simp add: i inf)
  1585       finally have ai: "a \<bullet> i \<le> x \<bullet> i" .
  1586       have "x \<bullet> i \<le> (SUP x\<in>S. x \<bullet> i)"
  1587         by (simp add: i sup)
  1588       also have "(SUP x\<in>S. x \<bullet> i) \<le> b \<bullet> i"
  1589         by (simp add: False b cSUP_least)
  1590       finally have bi: "x \<bullet> i \<le> b \<bullet> i" .
  1591       show "x \<bullet> i \<in> (\<lambda>x. x \<bullet> i) ` S"
  1592         apply (rule_tac x="\<Sum>j\<in>Basis. (if j = i then x \<bullet> i else a \<bullet> j) *\<^sub>R j" in image_eqI)
  1593         apply (simp add: i)
  1594         apply (rule mem_is_intervalI [OF \<open>is_interval S\<close> \<open>a \<in> S\<close> \<open>b \<in> S\<close>])
  1595         using i ai bi apply force
  1596         done
  1597     qed
  1598     have "S = cbox a b"
  1599       by (auto simp: a_def b_def mem_box intro: 1 2 3)
  1600     then show ?rhs
  1601       by blast
  1602   next
  1603     assume R: ?rhs
  1604     then show ?lhs
  1605       using compact_cbox is_interval_cbox by blast
  1606   qed
  1607 qed
  1608 
  1609 
  1610 subsection%unimportant\<open>Componentwise limits and continuity\<close>
  1611 
  1612 text\<open>But is the premise really necessary? Need to generalise @{thm euclidean_dist_l2}\<close>
  1613 lemma Euclidean_dist_upper: "i \<in> Basis \<Longrightarrow> dist (x \<bullet> i) (y \<bullet> i) \<le> dist x y"
  1614   by (metis (no_types) member_le_L2_set euclidean_dist_l2 finite_Basis)
  1615 
  1616 text\<open>But is the premise \<^term>\<open>i \<in> Basis\<close> really necessary?\<close>
  1617 lemma open_preimage_inner:
  1618   assumes "open S" "i \<in> Basis"
  1619     shows "open {x. x \<bullet> i \<in> S}"
  1620 proof (rule openI, simp)
  1621   fix x
  1622   assume x: "x \<bullet> i \<in> S"
  1623   with assms obtain e where "0 < e" and e: "ball (x \<bullet> i) e \<subseteq> S"
  1624     by (auto simp: open_contains_ball_eq)
  1625   have "\<exists>e>0. ball (y \<bullet> i) e \<subseteq> S" if dxy: "dist x y < e / 2" for y
  1626   proof (intro exI conjI)
  1627     have "dist (x \<bullet> i) (y \<bullet> i) < e / 2"
  1628       by (meson \<open>i \<in> Basis\<close> dual_order.trans Euclidean_dist_upper not_le that)
  1629     then have "dist (x \<bullet> i) z < e" if "dist (y \<bullet> i) z < e / 2" for z
  1630       by (metis dist_commute dist_triangle_half_l that)
  1631     then have "ball (y \<bullet> i) (e / 2) \<subseteq> ball (x \<bullet> i) e"
  1632       using mem_ball by blast
  1633       with e show "ball (y \<bullet> i) (e / 2) \<subseteq> S"
  1634         by (metis order_trans)
  1635   qed (simp add: \<open>0 < e\<close>)
  1636   then show "\<exists>e>0. ball x e \<subseteq> {s. s \<bullet> i \<in> S}"
  1637     by (metis (no_types, lifting) \<open>0 < e\<close> \<open>open S\<close> half_gt_zero_iff mem_Collect_eq mem_ball open_contains_ball_eq subsetI)
  1638 qed
  1639 
  1640 proposition tendsto_componentwise_iff:
  1641   fixes f :: "_ \<Rightarrow> 'b::euclidean_space"
  1642   shows "(f \<longlongrightarrow> l) F \<longleftrightarrow> (\<forall>i \<in> Basis. ((\<lambda>x. (f x \<bullet> i)) \<longlongrightarrow> (l \<bullet> i)) F)"
  1643          (is "?lhs = ?rhs")
  1644 proof
  1645   assume ?lhs
  1646   then show ?rhs
  1647     unfolding tendsto_def
  1648     apply clarify
  1649     apply (drule_tac x="{s. s \<bullet> i \<in> S}" in spec)
  1650     apply (auto simp: open_preimage_inner)
  1651     done
  1652 next
  1653   assume R: ?rhs
  1654   then have "\<And>e. e > 0 \<Longrightarrow> \<forall>i\<in>Basis. \<forall>\<^sub>F x in F. dist (f x \<bullet> i) (l \<bullet> i) < e"
  1655     unfolding tendsto_iff by blast
  1656   then have R': "\<And>e. e > 0 \<Longrightarrow> \<forall>\<^sub>F x in F. \<forall>i\<in>Basis. dist (f x \<bullet> i) (l \<bullet> i) < e"
  1657       by (simp add: eventually_ball_finite_distrib [symmetric])
  1658   show ?lhs
  1659   unfolding tendsto_iff
  1660   proof clarify
  1661     fix e::real
  1662     assume "0 < e"
  1663     have *: "L2_set (\<lambda>i. dist (f x \<bullet> i) (l \<bullet> i)) Basis < e"
  1664              if "\<forall>i\<in>Basis. dist (f x \<bullet> i) (l \<bullet> i) < e / real DIM('b)" for x
  1665     proof -
  1666       have "L2_set (\<lambda>i. dist (f x \<bullet> i) (l \<bullet> i)) Basis \<le> sum (\<lambda>i. dist (f x \<bullet> i) (l \<bullet> i)) Basis"
  1667         by (simp add: L2_set_le_sum)
  1668       also have "... < DIM('b) * (e / real DIM('b))"
  1669         apply (rule sum_bounded_above_strict)
  1670         using that by auto
  1671       also have "... = e"
  1672         by (simp add: field_simps)
  1673       finally show "L2_set (\<lambda>i. dist (f x \<bullet> i) (l \<bullet> i)) Basis < e" .
  1674     qed
  1675     have "\<forall>\<^sub>F x in F. \<forall>i\<in>Basis. dist (f x \<bullet> i) (l \<bullet> i) < e / DIM('b)"
  1676       apply (rule R')
  1677       using \<open>0 < e\<close> by simp
  1678     then show "\<forall>\<^sub>F x in F. dist (f x) l < e"
  1679       apply (rule eventually_mono)
  1680       apply (subst euclidean_dist_l2)
  1681       using * by blast
  1682   qed
  1683 qed
  1684 
  1685 
  1686 corollary continuous_componentwise:
  1687    "continuous F f \<longleftrightarrow> (\<forall>i \<in> Basis. continuous F (\<lambda>x. (f x \<bullet> i)))"
  1688 by (simp add: continuous_def tendsto_componentwise_iff [symmetric])
  1689 
  1690 corollary continuous_on_componentwise:
  1691   fixes S :: "'a :: t2_space set"
  1692   shows "continuous_on S f \<longleftrightarrow> (\<forall>i \<in> Basis. continuous_on S (\<lambda>x. (f x \<bullet> i)))"
  1693   apply (simp add: continuous_on_eq_continuous_within)
  1694   using continuous_componentwise by blast
  1695 
  1696 lemma linear_componentwise_iff:
  1697      "(linear f') \<longleftrightarrow> (\<forall>i\<in>Basis. linear (\<lambda>x. f' x \<bullet> i))"
  1698   apply (auto simp: linear_iff inner_left_distrib)
  1699    apply (metis inner_left_distrib euclidean_eq_iff)
  1700   by (metis euclidean_eqI inner_scaleR_left)
  1701 
  1702 lemma bounded_linear_componentwise_iff:
  1703      "(bounded_linear f') \<longleftrightarrow> (\<forall>i\<in>Basis. bounded_linear (\<lambda>x. f' x \<bullet> i))"
  1704      (is "?lhs = ?rhs")
  1705 proof
  1706   assume ?lhs then show ?rhs
  1707     by (simp add: bounded_linear_inner_left_comp)
  1708 next
  1709   assume ?rhs
  1710   then have "(\<forall>i\<in>Basis. \<exists>K. \<forall>x. \<bar>f' x \<bullet> i\<bar> \<le> norm x * K)" "linear f'"
  1711     by (auto simp: bounded_linear_def bounded_linear_axioms_def linear_componentwise_iff [symmetric] ball_conj_distrib)
  1712   then obtain F where F: "\<And>i x. i \<in> Basis \<Longrightarrow> \<bar>f' x \<bullet> i\<bar> \<le> norm x * F i"
  1713     by metis
  1714   have "norm (f' x) \<le> norm x * sum F Basis" for x
  1715   proof -
  1716     have "norm (f' x) \<le> (\<Sum>i\<in>Basis. \<bar>f' x \<bullet> i\<bar>)"
  1717       by (rule norm_le_l1)
  1718     also have "... \<le> (\<Sum>i\<in>Basis. norm x * F i)"
  1719       by (metis F sum_mono)
  1720     also have "... = norm x * sum F Basis"
  1721       by (simp add: sum_distrib_left)
  1722     finally show ?thesis .
  1723   qed
  1724   then show ?lhs
  1725     by (force simp: bounded_linear_def bounded_linear_axioms_def \<open>linear f'\<close>)
  1726 qed
  1727 
  1728 subsection%unimportant \<open>Continuous Extension\<close>
  1729 
  1730 definition clamp :: "'a::euclidean_space \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" where
  1731   "clamp a b x = (if (\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i)
  1732     then (\<Sum>i\<in>Basis. (if x\<bullet>i < a\<bullet>i then a\<bullet>i else if x\<bullet>i \<le> b\<bullet>i then x\<bullet>i else b\<bullet>i) *\<^sub>R i)
  1733     else a)"
  1734 
  1735 lemma clamp_in_interval[simp]:
  1736   assumes "\<And>i. i \<in> Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i"
  1737   shows "clamp a b x \<in> cbox a b"
  1738   unfolding clamp_def
  1739   using box_ne_empty(1)[of a b] assms by (auto simp: cbox_def)
  1740 
  1741 lemma clamp_cancel_cbox[simp]:
  1742   fixes x a b :: "'a::euclidean_space"
  1743   assumes x: "x \<in> cbox a b"
  1744   shows "clamp a b x = x"
  1745   using assms
  1746   by (auto simp: clamp_def mem_box intro!: euclidean_eqI[where 'a='a])
  1747 
  1748 lemma clamp_empty_interval:
  1749   assumes "i \<in> Basis" "a \<bullet> i > b \<bullet> i"
  1750   shows "clamp a b = (\<lambda>_. a)"
  1751   using assms
  1752   by (force simp: clamp_def[abs_def] split: if_splits intro!: ext)
  1753 
  1754 lemma dist_clamps_le_dist_args:
  1755   fixes x :: "'a::euclidean_space"
  1756   shows "dist (clamp a b y) (clamp a b x) \<le> dist y x"
  1757 proof cases
  1758   assume le: "(\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i)"
  1759   then have "(\<Sum>i\<in>Basis. (dist (clamp a b y \<bullet> i) (clamp a b x \<bullet> i))\<^sup>2) \<le>
  1760     (\<Sum>i\<in>Basis. (dist (y \<bullet> i) (x \<bullet> i))\<^sup>2)"
  1761     by (auto intro!: sum_mono simp: clamp_def dist_real_def abs_le_square_iff[symmetric])
  1762   then show ?thesis
  1763     by (auto intro: real_sqrt_le_mono
  1764       simp: euclidean_dist_l2[where y=x] euclidean_dist_l2[where y="clamp a b x"] L2_set_def)
  1765 qed (auto simp: clamp_def)
  1766 
  1767 lemma clamp_continuous_at:
  1768   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::metric_space"
  1769     and x :: 'a
  1770   assumes f_cont: "continuous_on (cbox a b) f"
  1771   shows "continuous (at x) (\<lambda>x. f (clamp a b x))"
  1772 proof cases
  1773   assume le: "(\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i)"
  1774   show ?thesis
  1775     unfolding continuous_at_eps_delta
  1776   proof safe
  1777     fix x :: 'a
  1778     fix e :: real
  1779     assume "e > 0"
  1780     moreover have "clamp a b x \<in> cbox a b"
  1781       by (simp add: clamp_in_interval le)
  1782     moreover note f_cont[simplified continuous_on_iff]
  1783     ultimately
  1784     obtain d where d: "0 < d"
  1785       "\<And>x'. x' \<in> cbox a b \<Longrightarrow> dist x' (clamp a b x) < d \<Longrightarrow> dist (f x') (f (clamp a b x)) < e"
  1786       by force
  1787     show "\<exists>d>0. \<forall>x'. dist x' x < d \<longrightarrow>
  1788       dist (f (clamp a b x')) (f (clamp a b x)) < e"
  1789       using le
  1790       by (auto intro!: d clamp_in_interval dist_clamps_le_dist_args[THEN le_less_trans])
  1791   qed
  1792 qed (auto simp: clamp_empty_interval)
  1793 
  1794 lemma clamp_continuous_on:
  1795   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::metric_space"
  1796   assumes f_cont: "continuous_on (cbox a b) f"
  1797   shows "continuous_on S (\<lambda>x. f (clamp a b x))"
  1798   using assms
  1799   by (auto intro: continuous_at_imp_continuous_on clamp_continuous_at)
  1800 
  1801 lemma clamp_bounded:
  1802   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::metric_space"
  1803   assumes bounded: "bounded (f ` (cbox a b))"
  1804   shows "bounded (range (\<lambda>x. f (clamp a b x)))"
  1805 proof cases
  1806   assume le: "(\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i)"
  1807   from bounded obtain c where f_bound: "\<forall>x\<in>f ` cbox a b. dist undefined x \<le> c"
  1808     by (auto simp: bounded_any_center[where a=undefined])
  1809   then show ?thesis
  1810     by (auto intro!: exI[where x=c] clamp_in_interval[OF le[rule_format]]
  1811         simp: bounded_any_center[where a=undefined])
  1812 qed (auto simp: clamp_empty_interval image_def)
  1813 
  1814 
  1815 definition ext_cont :: "('a::euclidean_space \<Rightarrow> 'b::metric_space) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b"
  1816   where "ext_cont f a b = (\<lambda>x. f (clamp a b x))"
  1817 
  1818 lemma ext_cont_cancel_cbox[simp]:
  1819   fixes x a b :: "'a::euclidean_space"
  1820   assumes x: "x \<in> cbox a b"
  1821   shows "ext_cont f a b x = f x"
  1822   using assms
  1823   unfolding ext_cont_def
  1824   by (auto simp: clamp_def mem_box intro!: euclidean_eqI[where 'a='a] arg_cong[where f=f])
  1825 
  1826 lemma continuous_on_ext_cont[continuous_intros]:
  1827   "continuous_on (cbox a b) f \<Longrightarrow> continuous_on S (ext_cont f a b)"
  1828   by (auto intro!: clamp_continuous_on simp: ext_cont_def)
  1829 
  1830 
  1831 subsection \<open>Separability\<close>
  1832 
  1833 lemma univ_second_countable_sequence:
  1834   obtains B :: "nat \<Rightarrow> 'a::euclidean_space set"
  1835     where "inj B" "\<And>n. open(B n)" "\<And>S. open S \<Longrightarrow> \<exists>k. S = \<Union>{B n |n. n \<in> k}"
  1836 proof -
  1837   obtain \<B> :: "'a set set"
  1838   where "countable \<B>"
  1839     and opn: "\<And>C. C \<in> \<B> \<Longrightarrow> open C"
  1840     and Un: "\<And>S. open S \<Longrightarrow> \<exists>U. U \<subseteq> \<B> \<and> S = \<Union>U"
  1841     using univ_second_countable by blast
  1842   have *: "infinite (range (\<lambda>n. ball (0::'a) (inverse(Suc n))))"
  1843     apply (rule Infinite_Set.range_inj_infinite)
  1844     apply (simp add: inj_on_def ball_eq_ball_iff)
  1845     done
  1846   have "infinite \<B>"
  1847   proof
  1848     assume "finite \<B>"
  1849     then have "finite (Union ` (Pow \<B>))"
  1850       by simp
  1851     then have "finite (range (\<lambda>n. ball (0::'a) (inverse(Suc n))))"
  1852       apply (rule rev_finite_subset)
  1853       by (metis (no_types, lifting) PowI image_eqI image_subset_iff Un [OF open_ball])
  1854     with * show False by simp
  1855   qed
  1856   obtain f :: "nat \<Rightarrow> 'a set" where "\<B> = range f" "inj f"
  1857     by (blast intro: countable_as_injective_image [OF \<open>countable \<B>\<close> \<open>infinite \<B>\<close>])
  1858   have *: "\<exists>k. S = \<Union>{f n |n. n \<in> k}" if "open S" for S
  1859     using Un [OF that]
  1860     apply clarify
  1861     apply (rule_tac x="f-`U" in exI)
  1862     using \<open>inj f\<close> \<open>\<B> = range f\<close> apply force
  1863     done
  1864   show ?thesis
  1865     apply (rule that [OF \<open>inj f\<close> _ *])
  1866     apply (auto simp: \<open>\<B> = range f\<close> opn)
  1867     done
  1868 qed
  1869 
  1870 proposition separable:
  1871   fixes S :: "'a::{metric_space, second_countable_topology} set"
  1872   obtains T where "countable T" "T \<subseteq> S" "S \<subseteq> closure T"
  1873 proof -
  1874   obtain \<B> :: "'a set set"
  1875     where "countable \<B>"
  1876       and "{} \<notin> \<B>"
  1877       and ope: "\<And>C. C \<in> \<B> \<Longrightarrow> openin(top_of_set S) C"
  1878       and if_ope: "\<And>T. openin(top_of_set S) T \<Longrightarrow> \<exists>\<U>. \<U> \<subseteq> \<B> \<and> T = \<Union>\<U>"
  1879     by (meson subset_second_countable)
  1880   then obtain f where f: "\<And>C. C \<in> \<B> \<Longrightarrow> f C \<in> C"
  1881     by (metis equals0I)
  1882   show ?thesis
  1883   proof
  1884     show "countable (f ` \<B>)"
  1885       by (simp add: \<open>countable \<B>\<close>)
  1886     show "f ` \<B> \<subseteq> S"
  1887       using ope f openin_imp_subset by blast
  1888     show "S \<subseteq> closure (f ` \<B>)"
  1889     proof (clarsimp simp: closure_approachable)
  1890       fix x and e::real
  1891       assume "x \<in> S" "0 < e"
  1892       have "openin (top_of_set S) (S \<inter> ball x e)"
  1893         by (simp add: openin_Int_open)
  1894       with if_ope obtain \<U> where  \<U>: "\<U> \<subseteq> \<B>" "S \<inter> ball x e = \<Union>\<U>"
  1895         by meson
  1896       show "\<exists>C \<in> \<B>. dist (f C) x < e"
  1897       proof (cases "\<U> = {}")
  1898         case True
  1899         then show ?thesis
  1900           using \<open>0 < e\<close>  \<U> \<open>x \<in> S\<close> by auto
  1901       next
  1902         case False
  1903         then obtain C where "C \<in> \<U>" by blast
  1904         show ?thesis
  1905         proof
  1906           show "dist (f C) x < e"
  1907             by (metis Int_iff Union_iff \<U> \<open>C \<in> \<U>\<close> dist_commute f mem_ball subsetCE)
  1908           show "C \<in> \<B>"
  1909             using \<open>\<U> \<subseteq> \<B>\<close> \<open>C \<in> \<U>\<close> by blast
  1910         qed
  1911       qed
  1912     qed
  1913   qed
  1914 qed
  1915 
  1916 
  1917 subsection%unimportant \<open>Diameter\<close>
  1918 
  1919 lemma diameter_cball [simp]:
  1920   fixes a :: "'a::euclidean_space"
  1921   shows "diameter(cball a r) = (if r < 0 then 0 else 2*r)"
  1922 proof -
  1923   have "diameter(cball a r) = 2*r" if "r \<ge> 0"
  1924   proof (rule order_antisym)
  1925     show "diameter (cball a r) \<le> 2*r"
  1926     proof (rule diameter_le)
  1927       fix x y assume "x \<in> cball a r" "y \<in> cball a r"
  1928       then have "norm (x - a) \<le> r" "norm (a - y) \<le> r"
  1929         by (auto simp: dist_norm norm_minus_commute)
  1930       then have "norm (x - y) \<le> r+r"
  1931         using norm_diff_triangle_le by blast
  1932       then show "norm (x - y) \<le> 2*r" by simp
  1933     qed (simp add: that)
  1934     have "2*r = dist (a + r *\<^sub>R (SOME i. i \<in> Basis)) (a - r *\<^sub>R (SOME i. i \<in> Basis))"
  1935       apply (simp add: dist_norm)
  1936       by (metis abs_of_nonneg mult.right_neutral norm_numeral norm_scaleR norm_some_Basis real_norm_def scaleR_2 that)
  1937     also have "... \<le> diameter (cball a r)"
  1938       apply (rule diameter_bounded_bound)
  1939       using that by (auto simp: dist_norm)
  1940     finally show "2*r \<le> diameter (cball a r)" .
  1941   qed
  1942   then show ?thesis by simp
  1943 qed
  1944 
  1945 lemma diameter_ball [simp]:
  1946   fixes a :: "'a::euclidean_space"
  1947   shows "diameter(ball a r) = (if r < 0 then 0 else 2*r)"
  1948 proof -
  1949   have "diameter(ball a r) = 2*r" if "r > 0"
  1950     by (metis bounded_ball diameter_closure closure_ball diameter_cball less_eq_real_def linorder_not_less that)
  1951   then show ?thesis
  1952     by (simp add: diameter_def)
  1953 qed
  1954 
  1955 lemma diameter_closed_interval [simp]: "diameter {a..b} = (if b < a then 0 else b-a)"
  1956 proof -
  1957   have "{a .. b} = cball ((a+b)/2) ((b-a)/2)"
  1958     by (auto simp: dist_norm abs_if divide_simps split: if_split_asm)
  1959   then show ?thesis
  1960     by simp
  1961 qed
  1962 
  1963 lemma diameter_open_interval [simp]: "diameter {a<..<b} = (if b < a then 0 else b-a)"
  1964 proof -
  1965   have "{a <..< b} = ball ((a+b)/2) ((b-a)/2)"
  1966     by (auto simp: dist_norm abs_if divide_simps split: if_split_asm)
  1967   then show ?thesis
  1968     by simp
  1969 qed
  1970 
  1971 lemma diameter_cbox:
  1972   fixes a b::"'a::euclidean_space"
  1973   shows "(\<forall>i \<in> Basis. a \<bullet> i \<le> b \<bullet> i) \<Longrightarrow> diameter (cbox a b) = dist a b"
  1974   by (force simp: diameter_def intro!: cSup_eq_maximum L2_set_mono
  1975      simp: euclidean_dist_l2[where 'a='a] cbox_def dist_norm)
  1976 
  1977 
  1978 subsection%unimportant\<open>Relating linear images to open/closed/interior/closure/connected\<close>
  1979 
  1980 proposition open_surjective_linear_image:
  1981   fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::euclidean_space"
  1982   assumes "open A" "linear f" "surj f"
  1983     shows "open(f ` A)"
  1984 unfolding open_dist
  1985 proof clarify
  1986   fix x
  1987   assume "x \<in> A"
  1988   have "bounded (inv f ` Basis)"
  1989     by (simp add: finite_imp_bounded)
  1990   with bounded_pos obtain B where "B > 0" and B: "\<And>x. x \<in> inv f ` Basis \<Longrightarrow> norm x \<le> B"
  1991     by metis
  1992   obtain e where "e > 0" and e: "\<And>z. dist z x < e \<Longrightarrow> z \<in> A"
  1993     by (metis open_dist \<open>x \<in> A\<close> \<open>open A\<close>)
  1994   define \<delta> where "\<delta> \<equiv> e / B / DIM('b)"
  1995   show "\<exists>e>0. \<forall>y. dist y (f x) < e \<longrightarrow> y \<in> f ` A"
  1996   proof (intro exI conjI)
  1997     show "\<delta> > 0"
  1998       using \<open>e > 0\<close> \<open>B > 0\<close>  by (simp add: \<delta>_def divide_simps)
  1999     have "y \<in> f ` A" if "dist y (f x) * (B * real DIM('b)) < e" for y
  2000     proof -
  2001       define u where "u \<equiv> y - f x"
  2002       show ?thesis
  2003       proof (rule image_eqI)
  2004         show "y = f (x + (\<Sum>i\<in>Basis. (u \<bullet> i) *\<^sub>R inv f i))"
  2005           apply (simp add: linear_add linear_sum linear.scaleR \<open>linear f\<close> surj_f_inv_f \<open>surj f\<close>)
  2006           apply (simp add: euclidean_representation u_def)
  2007           done
  2008         have "dist (x + (\<Sum>i\<in>Basis. (u \<bullet> i) *\<^sub>R inv f i)) x \<le> (\<Sum>i\<in>Basis. norm ((u \<bullet> i) *\<^sub>R inv f i))"
  2009           by (simp add: dist_norm sum_norm_le)
  2010         also have "... = (\<Sum>i\<in>Basis. \<bar>u \<bullet> i\<bar> * norm (inv f i))"
  2011           by simp
  2012         also have "... \<le> (\<Sum>i\<in>Basis. \<bar>u \<bullet> i\<bar>) * B"
  2013           by (simp add: B sum_distrib_right sum_mono mult_left_mono)
  2014         also have "... \<le> DIM('b) * dist y (f x) * B"
  2015           apply (rule mult_right_mono [OF sum_bounded_above])
  2016           using \<open>0 < B\<close> by (auto simp: Basis_le_norm dist_norm u_def)
  2017         also have "... < e"
  2018           by (metis mult.commute mult.left_commute that)
  2019         finally show "x + (\<Sum>i\<in>Basis. (u \<bullet> i) *\<^sub>R inv f i) \<in> A"
  2020           by (rule e)
  2021       qed
  2022     qed
  2023     then show "\<forall>y. dist y (f x) < \<delta> \<longrightarrow> y \<in> f ` A"
  2024       using \<open>e > 0\<close> \<open>B > 0\<close>
  2025       by (auto simp: \<delta>_def divide_simps mult_less_0_iff)
  2026   qed
  2027 qed
  2028 
  2029 corollary open_bijective_linear_image_eq:
  2030   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
  2031   assumes "linear f" "bij f"
  2032     shows "open(f ` A) \<longleftrightarrow> open A"
  2033 proof
  2034   assume "open(f ` A)"
  2035   then have "open(f -` (f ` A))"
  2036     using assms by (force simp: linear_continuous_at linear_conv_bounded_linear continuous_open_vimage)
  2037   then show "open A"
  2038     by (simp add: assms bij_is_inj inj_vimage_image_eq)
  2039 next
  2040   assume "open A"
  2041   then show "open(f ` A)"
  2042     by (simp add: assms bij_is_surj open_surjective_linear_image)
  2043 qed
  2044 
  2045 corollary interior_bijective_linear_image:
  2046   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
  2047   assumes "linear f" "bij f"
  2048   shows "interior (f ` S) = f ` interior S"  (is "?lhs = ?rhs")
  2049 proof safe
  2050   fix x
  2051   assume x: "x \<in> ?lhs"
  2052   then obtain T where "open T" and "x \<in> T" and "T \<subseteq> f ` S"
  2053     by (metis interiorE)
  2054   then show "x \<in> ?rhs"
  2055     by (metis (no_types, hide_lams) assms subsetD interior_maximal open_bijective_linear_image_eq subset_image_iff)
  2056 next
  2057   fix x
  2058   assume x: "x \<in> interior S"
  2059   then show "f x \<in> interior (f ` S)"
  2060     by (meson assms imageI image_mono interiorI interior_subset open_bijective_linear_image_eq open_interior)
  2061 qed
  2062 
  2063 lemma interior_injective_linear_image:
  2064   fixes f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space"
  2065   assumes "linear f" "inj f"
  2066    shows "interior(f ` S) = f ` (interior S)"
  2067   by (simp add: linear_injective_imp_surjective assms bijI interior_bijective_linear_image)
  2068 
  2069 lemma interior_surjective_linear_image:
  2070   fixes f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space"
  2071   assumes "linear f" "surj f"
  2072    shows "interior(f ` S) = f ` (interior S)"
  2073   by (simp add: assms interior_injective_linear_image linear_surjective_imp_injective)
  2074 
  2075 lemma interior_negations:
  2076   fixes S :: "'a::euclidean_space set"
  2077   shows "interior(uminus ` S) = image uminus (interior S)"
  2078   by (simp add: bij_uminus interior_bijective_linear_image linear_uminus)
  2079 
  2080 lemma connected_linear_image:
  2081   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
  2082   assumes "linear f" and "connected s"
  2083   shows "connected (f ` s)"
  2084 using connected_continuous_image assms linear_continuous_on linear_conv_bounded_linear by blast
  2085 
  2086 
  2087 subsection%unimportant \<open>"Isometry" (up to constant bounds) of Injective Linear Map\<close>
  2088 
  2089 proposition injective_imp_isometric:
  2090   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
  2091   assumes s: "closed s" "subspace s"
  2092     and f: "bounded_linear f" "\<forall>x\<in>s. f x = 0 \<longrightarrow> x = 0"
  2093   shows "\<exists>e>0. \<forall>x\<in>s. norm (f x) \<ge> e * norm x"
  2094 proof (cases "s \<subseteq> {0::'a}")
  2095   case True
  2096   have "norm x \<le> norm (f x)" if "x \<in> s" for x
  2097   proof -
  2098     from True that have "x = 0" by auto
  2099     then show ?thesis by simp
  2100   qed
  2101   then show ?thesis
  2102     by (auto intro!: exI[where x=1])
  2103 next
  2104   case False
  2105   interpret f: bounded_linear f by fact
  2106   from False obtain a where a: "a \<noteq> 0" "a \<in> s"
  2107     by auto
  2108   from False have "s \<noteq> {}"
  2109     by auto
  2110   let ?S = "{f x| x. x \<in> s \<and> norm x = norm a}"
  2111   let ?S' = "{x::'a. x\<in>s \<and> norm x = norm a}"
  2112   let ?S'' = "{x::'a. norm x = norm a}"
  2113 
  2114   have "?S'' = frontier (cball 0 (norm a))"
  2115     by (simp add: sphere_def dist_norm)
  2116   then have "compact ?S''" by (metis compact_cball compact_frontier)
  2117   moreover have "?S' = s \<inter> ?S''" by auto
  2118   ultimately have "compact ?S'"
  2119     using closed_Int_compact[of s ?S''] using s(1) by auto
  2120   moreover have *:"f ` ?S' = ?S" by auto
  2121   ultimately have "compact ?S"
  2122     using compact_continuous_image[OF linear_continuous_on[OF f(1)], of ?S'] by auto
  2123   then have "closed ?S"
  2124     using compact_imp_closed by auto
  2125   moreover from a have "?S \<noteq> {}" by auto
  2126   ultimately obtain b' where "b'\<in>?S" "\<forall>y\<in>?S. norm b' \<le> norm y"
  2127     using distance_attains_inf[of ?S 0] unfolding dist_0_norm by auto
  2128   then obtain b where "b\<in>s"
  2129     and ba: "norm b = norm a"
  2130     and b: "\<forall>x\<in>{x \<in> s. norm x = norm a}. norm (f b) \<le> norm (f x)"
  2131     unfolding *[symmetric] unfolding image_iff by auto
  2132 
  2133   let ?e = "norm (f b) / norm b"
  2134   have "norm b > 0"
  2135     using ba and a and norm_ge_zero by auto
  2136   moreover have "norm (f b) > 0"
  2137     using f(2)[THEN bspec[where x=b], OF \<open>b\<in>s\<close>]
  2138     using \<open>norm b >0\<close> by simp
  2139   ultimately have "0 < norm (f b) / norm b" by simp
  2140   moreover
  2141   have "norm (f b) / norm b * norm x \<le> norm (f x)" if "x\<in>s" for x
  2142   proof (cases "x = 0")
  2143     case True
  2144     then show "norm (f b) / norm b * norm x \<le> norm (f x)"
  2145       by auto
  2146   next
  2147     case False
  2148     with \<open>a \<noteq> 0\<close> have *: "0 < norm a / norm x"
  2149       unfolding zero_less_norm_iff[symmetric] by simp
  2150     have "\<forall>x\<in>s. c *\<^sub>R x \<in> s" for c
  2151       using s[unfolded subspace_def] by simp
  2152     with \<open>x \<in> s\<close> \<open>x \<noteq> 0\<close> have "(norm a / norm x) *\<^sub>R x \<in> {x \<in> s. norm x = norm a}"
  2153       by simp
  2154     with \<open>x \<noteq> 0\<close> \<open>a \<noteq> 0\<close> show "norm (f b) / norm b * norm x \<le> norm (f x)"
  2155       using b[THEN bspec[where x="(norm a / norm x) *\<^sub>R x"]]
  2156       unfolding f.scaleR and ba
  2157       by (auto simp: mult.commute pos_le_divide_eq pos_divide_le_eq)
  2158   qed
  2159   ultimately show ?thesis by auto
  2160 qed
  2161 
  2162 proposition closed_injective_image_subspace:
  2163   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
  2164   assumes "subspace s" "bounded_linear f" "\<forall>x\<in>s. f x = 0 \<longrightarrow> x = 0" "closed s"
  2165   shows "closed(f ` s)"
  2166 proof -
  2167   obtain e where "e > 0" and e: "\<forall>x\<in>s. e * norm x \<le> norm (f x)"
  2168     using injective_imp_isometric[OF assms(4,1,2,3)] by auto
  2169   show ?thesis
  2170     using complete_isometric_image[OF \<open>e>0\<close> assms(1,2) e] and assms(4)
  2171     unfolding complete_eq_closed[symmetric] by auto
  2172 qed
  2173 
  2174 
  2175 subsection%unimportant \<open>Some properties of a canonical subspace\<close>
  2176 
  2177 lemma closed_substandard: "closed {x::'a::euclidean_space. \<forall>i\<in>Basis. P i \<longrightarrow> x\<bullet>i = 0}"
  2178   (is "closed ?A")
  2179 proof -
  2180   let ?D = "{i\<in>Basis. P i}"
  2181   have "closed (\<Inter>i\<in>?D. {x::'a. x\<bullet>i = 0})"
  2182     by (simp add: closed_INT closed_Collect_eq continuous_on_inner
  2183         continuous_on_const continuous_on_id)
  2184   also have "(\<Inter>i\<in>?D. {x::'a. x\<bullet>i = 0}) = ?A"
  2185     by auto
  2186   finally show "closed ?A" .
  2187 qed
  2188 
  2189 lemma closed_subspace:
  2190   fixes s :: "'a::euclidean_space set"
  2191   assumes "subspace s"
  2192   shows "closed s"
  2193 proof -
  2194   have "dim s \<le> card (Basis :: 'a set)"
  2195     using dim_subset_UNIV by auto
  2196   with ex_card[OF this] obtain d :: "'a set" where t: "card d = dim s" and d: "d \<subseteq> Basis"
  2197     by auto
  2198   let ?t = "{x::'a. \<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x\<bullet>i = 0}"
  2199   have "\<exists>f. linear f \<and> f ` {x::'a. \<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x \<bullet> i = 0} = s \<and>
  2200       inj_on f {x::'a. \<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x \<bullet> i = 0}"
  2201     using dim_substandard[of d] t d assms
  2202     by (intro subspace_isomorphism[OF subspace_substandard[of "\<lambda>i. i \<notin> d"]]) (auto simp: inner_Basis)
  2203   then obtain f where f:
  2204       "linear f"
  2205       "f ` {x. \<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x \<bullet> i = 0} = s"
  2206       "inj_on f {x. \<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x \<bullet> i = 0}"
  2207     by blast
  2208   interpret f: bounded_linear f
  2209     using f by (simp add: linear_conv_bounded_linear)
  2210   have "x \<in> ?t \<Longrightarrow> f x = 0 \<Longrightarrow> x = 0" for x
  2211     using f.zero d f(3)[THEN inj_onD, of x 0] by auto
  2212   moreover have "closed ?t" by (rule closed_substandard)
  2213   moreover have "subspace ?t" by (rule subspace_substandard)
  2214   ultimately show ?thesis
  2215     using closed_injective_image_subspace[of ?t f]
  2216     unfolding f(2) using f(1) unfolding linear_conv_bounded_linear by auto
  2217 qed
  2218 
  2219 lemma complete_subspace: "subspace s \<Longrightarrow> complete s"
  2220   for s :: "'a::euclidean_space set"
  2221   using complete_eq_closed closed_subspace by auto
  2222 
  2223 lemma closed_span [iff]: "closed (span s)"
  2224   for s :: "'a::euclidean_space set"
  2225   by (simp add: closed_subspace subspace_span)
  2226 
  2227 lemma dim_closure [simp]: "dim (closure s) = dim s" (is "?dc = ?d")
  2228   for s :: "'a::euclidean_space set"
  2229 proof -
  2230   have "?dc \<le> ?d"
  2231     using closure_minimal[OF span_superset, of s]
  2232     using closed_subspace[OF subspace_span, of s]
  2233     using dim_subset[of "closure s" "span s"]
  2234     by simp
  2235   then show ?thesis
  2236     using dim_subset[OF closure_subset, of s]
  2237     by simp
  2238 qed
  2239 
  2240 
  2241 subsection \<open>Set Distance\<close>
  2242 
  2243 lemma setdist_compact_closed:
  2244   fixes A :: "'a::heine_borel set"
  2245   assumes A: "compact A" and B: "closed B"
  2246     and "A \<noteq> {}" "B \<noteq> {}"
  2247   shows "\<exists>x \<in> A. \<exists>y \<in> B. dist x y = setdist A B"
  2248 proof -
  2249   obtain x where "x \<in> A" "setdist A B = infdist x B"
  2250     by (metis A assms(3) setdist_attains_inf setdist_sym)
  2251   moreover
  2252   obtain y where"y \<in> B" "infdist x B = dist x y"
  2253     using B \<open>B \<noteq> {}\<close> infdist_attains_inf by blast
  2254   ultimately show ?thesis
  2255     using \<open>x \<in> A\<close> \<open>y \<in> B\<close> by auto
  2256 qed
  2257 
  2258 lemma setdist_closed_compact:
  2259   fixes S :: "'a::heine_borel set"
  2260   assumes S: "closed S" and T: "compact T"
  2261       and "S \<noteq> {}" "T \<noteq> {}"
  2262     shows "\<exists>x \<in> S. \<exists>y \<in> T. dist x y = setdist S T"
  2263   using setdist_compact_closed [OF T S \<open>T \<noteq> {}\<close> \<open>S \<noteq> {}\<close>]
  2264   by (metis dist_commute setdist_sym)
  2265 
  2266 lemma setdist_eq_0_compact_closed:
  2267   assumes S: "compact S" and T: "closed T"
  2268     shows "setdist S T = 0 \<longleftrightarrow> S = {} \<or> T = {} \<or> S \<inter> T \<noteq> {}"
  2269 proof (cases "S = {} \<or> T = {}")
  2270   case True
  2271   then show ?thesis
  2272     by force
  2273 next
  2274   case False
  2275   then show ?thesis
  2276     by (metis S T disjoint_iff_not_equal in_closed_iff_infdist_zero setdist_attains_inf setdist_eq_0I setdist_sym)
  2277 qed
  2278 
  2279 corollary setdist_gt_0_compact_closed:
  2280   assumes S: "compact S" and T: "closed T"
  2281     shows "setdist S T > 0 \<longleftrightarrow> (S \<noteq> {} \<and> T \<noteq> {} \<and> S \<inter> T = {})"
  2282   using setdist_pos_le [of S T] setdist_eq_0_compact_closed [OF assms] by linarith
  2283 
  2284 lemma setdist_eq_0_closed_compact:
  2285   assumes S: "closed S" and T: "compact T"
  2286     shows "setdist S T = 0 \<longleftrightarrow> S = {} \<or> T = {} \<or> S \<inter> T \<noteq> {}"
  2287   using setdist_eq_0_compact_closed [OF T S]
  2288   by (metis Int_commute setdist_sym)
  2289 
  2290 lemma setdist_eq_0_bounded:
  2291   fixes S :: "'a::heine_borel set"
  2292   assumes "bounded S \<or> bounded T"
  2293   shows "setdist S T = 0 \<longleftrightarrow> S = {} \<or> T = {} \<or> closure S \<inter> closure T \<noteq> {}"
  2294 proof (cases "S = {} \<or> T = {}")
  2295   case False
  2296   then show ?thesis
  2297     using setdist_eq_0_compact_closed [of "closure S" "closure T"]
  2298           setdist_eq_0_closed_compact [of "closure S" "closure T"] assms
  2299     by (force simp:  bounded_closure compact_eq_bounded_closed)
  2300 qed force
  2301 
  2302 lemma setdist_eq_0_sing_1:
  2303   "setdist {x} S = 0 \<longleftrightarrow> S = {} \<or> x \<in> closure S"
  2304   by (metis in_closure_iff_infdist_zero infdist_def infdist_eq_setdist)
  2305 
  2306 lemma setdist_eq_0_sing_2:
  2307   "setdist S {x} = 0 \<longleftrightarrow> S = {} \<or> x \<in> closure S"
  2308   by (metis setdist_eq_0_sing_1 setdist_sym)
  2309 
  2310 lemma setdist_neq_0_sing_1:
  2311   "\<lbrakk>setdist {x} S = a; a \<noteq> 0\<rbrakk> \<Longrightarrow> S \<noteq> {} \<and> x \<notin> closure S"
  2312   by (metis setdist_closure_2 setdist_empty2 setdist_eq_0I singletonI)
  2313 
  2314 lemma setdist_neq_0_sing_2:
  2315   "\<lbrakk>setdist S {x} = a; a \<noteq> 0\<rbrakk> \<Longrightarrow> S \<noteq> {} \<and> x \<notin> closure S"
  2316   by (simp add: setdist_neq_0_sing_1 setdist_sym)
  2317 
  2318 lemma setdist_sing_in_set:
  2319    "x \<in> S \<Longrightarrow> setdist {x} S = 0"
  2320   by (simp add: setdist_eq_0I)
  2321 
  2322 lemma setdist_eq_0_closed:
  2323    "closed S \<Longrightarrow> (setdist {x} S = 0 \<longleftrightarrow> S = {} \<or> x \<in> S)"
  2324 by (simp add: setdist_eq_0_sing_1)
  2325 
  2326 lemma setdist_eq_0_closedin:
  2327   shows "\<lbrakk>closedin (top_of_set U) S; x \<in> U\<rbrakk>
  2328          \<Longrightarrow> (setdist {x} S = 0 \<longleftrightarrow> S = {} \<or> x \<in> S)"
  2329   by (auto simp: closedin_limpt setdist_eq_0_sing_1 closure_def)
  2330 
  2331 lemma setdist_gt_0_closedin:
  2332   shows "\<lbrakk>closedin (top_of_set U) S; x \<in> U; S \<noteq> {}; x \<notin> S\<rbrakk>
  2333          \<Longrightarrow> setdist {x} S > 0"
  2334   using less_eq_real_def setdist_eq_0_closedin by fastforce
  2335 
  2336 no_notation
  2337   eucl_less (infix "<e" 50)
  2338 
  2339 end