diff --git a/src/HOL/Analysis/Continuous_Extension.thy b/src/HOL/Analysis/Continuous_Extension.thy
--- a/src/HOL/Analysis/Continuous_Extension.thy
+++ b/src/HOL/Analysis/Continuous_Extension.thy
@@ -1,537 +1,551 @@
 (*  Title:      HOL/Analysis/Continuous_Extension.thy
     Authors:    LC Paulson, based on material from HOL Light
 *)
 
 section \<open>Continuous Extensions of Functions\<close>
 
 theory Continuous_Extension
 imports Starlike
 begin
 
 subsection\<open>Partitions of unity subordinate to locally finite open coverings\<close>
 
 text\<open>A difference from HOL Light: all summations over infinite sets equal zero,
    so the "support" must be made explicit in the summation below!\<close>
 
 proposition subordinate_partition_of_unity:
   fixes S :: "'a::metric_space set"
   assumes "S \<subseteq> \<Union>\<C>" and opC: "\<And>T. T \<in> \<C> \<Longrightarrow> open T"
       and fin: "\<And>x. x \<in> S \<Longrightarrow> \<exists>V. open V \<and> x \<in> V \<and> finite {U \<in> \<C>. U \<inter> V \<noteq> {}}"
   obtains F :: "['a set, 'a] \<Rightarrow> real"
     where "\<And>U. U \<in> \<C> \<Longrightarrow> continuous_on S (F U) \<and> (\<forall>x \<in> S. 0 \<le> F U x)"
       and "\<And>x U. \<lbrakk>U \<in> \<C>; x \<in> S; x \<notin> U\<rbrakk> \<Longrightarrow> F U x = 0"
       and "\<And>x. x \<in> S \<Longrightarrow> supp_sum (\<lambda>W. F W x) \<C> = 1"
       and "\<And>x. x \<in> S \<Longrightarrow> \<exists>V. open V \<and> x \<in> V \<and> finite {U \<in> \<C>. \<exists>x\<in>V. F U x \<noteq> 0}"
 proof (cases "\<exists>W. W \<in> \<C> \<and> S \<subseteq> W")
   case True
     then obtain W where "W \<in> \<C>" "S \<subseteq> W" by metis
     then show ?thesis
       by (rule_tac F = "\<lambda>V x. if V = W then 1 else 0" in that) (auto simp: supp_sum_def support_on_def)
 next
   case False
     have nonneg: "0 \<le> supp_sum (\<lambda>V. setdist {x} (S - V)) \<C>" for x
       by (simp add: supp_sum_def sum_nonneg)
     have sd_pos: "0 < setdist {x} (S - V)" if "V \<in> \<C>" "x \<in> S" "x \<in> V" for V x
     proof -
       have "closedin (top_of_set S) (S - V)"
         by (simp add: Diff_Diff_Int closedin_def opC openin_open_Int \<open>V \<in> \<C>\<close>)
       with that False  setdist_pos_le [of "{x}" "S - V"]
       show ?thesis
         using setdist_gt_0_closedin by fastforce
     qed
     have ss_pos: "0 < supp_sum (\<lambda>V. setdist {x} (S - V)) \<C>" if "x \<in> S" for x
     proof -
       obtain U where "U \<in> \<C>" "x \<in> U" using \<open>x \<in> S\<close> \<open>S \<subseteq> \<Union>\<C>\<close>
         by blast
       obtain V where "open V" "x \<in> V" "finite {U \<in> \<C>. U \<inter> V \<noteq> {}}"
         using \<open>x \<in> S\<close> fin by blast
       then have *: "finite {A \<in> \<C>. \<not> S \<subseteq> A \<and> x \<notin> closure (S - A)}"
         using closure_def that by (blast intro: rev_finite_subset)
       have "x \<notin> closure (S - U)"
         using \<open>U \<in> \<C>\<close> \<open>x \<in> U\<close> opC open_Int_closure_eq_empty by fastforce
       then show ?thesis
         apply (simp add: setdist_eq_0_sing_1 supp_sum_def support_on_def)
         apply (rule ordered_comm_monoid_add_class.sum_pos2 [OF *, of U])
         using \<open>U \<in> \<C>\<close> \<open>x \<in> U\<close> False
         apply (auto simp: sd_pos that)
         done
     qed
     define F where
       "F \<equiv> \<lambda>W x. if x \<in> S then setdist {x} (S - W) / supp_sum (\<lambda>V. setdist {x} (S - V)) \<C> else 0"
     show ?thesis
     proof (rule_tac F = F in that)
       have "continuous_on S (F U)" if "U \<in> \<C>" for U
       proof -
         have *: "continuous_on S (\<lambda>x. supp_sum (\<lambda>V. setdist {x} (S - V)) \<C>)"
         proof (clarsimp simp add: continuous_on_eq_continuous_within)
           fix x assume "x \<in> S"
           then obtain X where "open X" and x: "x \<in> S \<inter> X" and finX: "finite {U \<in> \<C>. U \<inter> X \<noteq> {}}"
             using assms by blast
           then have OSX: "openin (top_of_set S) (S \<inter> X)" by blast
           have sumeq: "\<And>x. x \<in> S \<inter> X \<Longrightarrow>
                      (\<Sum>V | V \<in> \<C> \<and> V \<inter> X \<noteq> {}. setdist {x} (S - V))
                      = supp_sum (\<lambda>V. setdist {x} (S - V)) \<C>"
             apply (simp add: supp_sum_def)
             apply (rule sum.mono_neutral_right [OF finX])
             apply (auto simp: setdist_eq_0_sing_1 support_on_def subset_iff)
             apply (meson DiffI closure_subset disjoint_iff_not_equal subsetCE)
             done
           show "continuous (at x within S) (\<lambda>x. supp_sum (\<lambda>V. setdist {x} (S - V)) \<C>)"
             apply (rule continuous_transform_within_openin
                      [where f = "\<lambda>x. (sum (\<lambda>V. setdist {x} (S - V)) {V \<in> \<C>. V \<inter> X \<noteq> {}})"
                         and S ="S \<inter> X"])
             apply (rule continuous_intros continuous_at_setdist continuous_at_imp_continuous_at_within OSX x)+
             apply (simp add: sumeq)
             done
         qed
         show ?thesis
           apply (simp add: F_def)
           apply (rule continuous_intros *)+
           using ss_pos apply force
           done
       qed
       moreover have "\<lbrakk>U \<in> \<C>; x \<in> S\<rbrakk> \<Longrightarrow> 0 \<le> F U x" for U x
         using nonneg [of x] by (simp add: F_def field_split_simps)
       ultimately show "\<And>U. U \<in> \<C> \<Longrightarrow> continuous_on S (F U) \<and> (\<forall>x\<in>S. 0 \<le> F U x)"
         by metis
     next
       show "\<And>x U. \<lbrakk>U \<in> \<C>; x \<in> S; x \<notin> U\<rbrakk> \<Longrightarrow> F U x = 0"
         by (simp add: setdist_eq_0_sing_1 closure_def F_def)
     next
       show "supp_sum (\<lambda>W. F W x) \<C> = 1" if "x \<in> S" for x
         using that ss_pos [OF that]
         by (simp add: F_def field_split_simps supp_sum_divide_distrib [symmetric])
     next
       show "\<exists>V. open V \<and> x \<in> V \<and> finite {U \<in> \<C>. \<exists>x\<in>V. F U x \<noteq> 0}" if "x \<in> S" for x
         using fin [OF that] that
         by (fastforce simp: setdist_eq_0_sing_1 closure_def F_def elim!: rev_finite_subset)
     qed
 qed
 
 
 subsection\<open>Urysohn's Lemma for Euclidean Spaces\<close>
 
 text \<open>For Euclidean spaces the proof is easy using distances.\<close>
 
 lemma Urysohn_both_ne:
   assumes US: "closedin (top_of_set U) S"
       and UT: "closedin (top_of_set U) T"
       and "S \<inter> T = {}" "S \<noteq> {}" "T \<noteq> {}" "a \<noteq> b"
   obtains f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
     where "continuous_on U f"
           "\<And>x. x \<in> U \<Longrightarrow> f x \<in> closed_segment a b"
           "\<And>x. x \<in> U \<Longrightarrow> (f x = a \<longleftrightarrow> x \<in> S)"
           "\<And>x. x \<in> U \<Longrightarrow> (f x = b \<longleftrightarrow> x \<in> T)"
 proof -
   have S0: "\<And>x. x \<in> U \<Longrightarrow> setdist {x} S = 0 \<longleftrightarrow> x \<in> S"
     using \<open>S \<noteq> {}\<close>  US setdist_eq_0_closedin  by auto
   have T0: "\<And>x. x \<in> U \<Longrightarrow> setdist {x} T = 0 \<longleftrightarrow> x \<in> T"
     using \<open>T \<noteq> {}\<close>  UT setdist_eq_0_closedin  by auto
   have sdpos: "0 < setdist {x} S + setdist {x} T" if "x \<in> U" for x
   proof -
     have "\<not> (setdist {x} S = 0 \<and> setdist {x} T = 0)"
       using assms by (metis IntI empty_iff setdist_eq_0_closedin that)
     then show ?thesis
       by (metis add.left_neutral add.right_neutral add_pos_pos linorder_neqE_linordered_idom not_le setdist_pos_le)
   qed
   define f where "f \<equiv> \<lambda>x. a + (setdist {x} S / (setdist {x} S + setdist {x} T)) *\<^sub>R (b - a)"
   show ?thesis
   proof (rule_tac f = f in that)
     show "continuous_on U f"
       using sdpos unfolding f_def
       by (intro continuous_intros | force)+
     show "f x \<in> closed_segment a b" if "x \<in> U" for x
         unfolding f_def
       apply (simp add: closed_segment_def)
       apply (rule_tac x="(setdist {x} S / (setdist {x} S + setdist {x} T))" in exI)
       using sdpos that apply (simp add: algebra_simps)
       done
     show "\<And>x. x \<in> U \<Longrightarrow> (f x = a \<longleftrightarrow> x \<in> S)"
       using S0 \<open>a \<noteq> b\<close> f_def sdpos by force
     show "(f x = b \<longleftrightarrow> x \<in> T)" if "x \<in> U" for x
     proof -
       have "f x = b \<longleftrightarrow> (setdist {x} S / (setdist {x} S + setdist {x} T)) = 1"
         unfolding f_def
         apply (rule iffI)
          apply (metis  \<open>a \<noteq> b\<close> add_diff_cancel_left' eq_iff_diff_eq_0 pth_1 real_vector.scale_right_imp_eq, force)
         done
       also have "...  \<longleftrightarrow> setdist {x} T = 0 \<and> setdist {x} S \<noteq> 0"
         using sdpos that
         by (simp add: field_split_simps) linarith
       also have "...  \<longleftrightarrow> x \<in> T"
         using \<open>S \<noteq> {}\<close> \<open>T \<noteq> {}\<close> \<open>S \<inter> T = {}\<close> that
         by (force simp: S0 T0)
       finally show ?thesis .
     qed
   qed
 qed
 
 proposition Urysohn_local_strong:
   assumes US: "closedin (top_of_set U) S"
       and UT: "closedin (top_of_set U) T"
       and "S \<inter> T = {}" "a \<noteq> b"
   obtains f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
     where "continuous_on U f"
           "\<And>x. x \<in> U \<Longrightarrow> f x \<in> closed_segment a b"
           "\<And>x. x \<in> U \<Longrightarrow> (f x = a \<longleftrightarrow> x \<in> S)"
           "\<And>x. x \<in> U \<Longrightarrow> (f x = b \<longleftrightarrow> x \<in> T)"
 proof (cases "S = {}")
   case True show ?thesis
   proof (cases "T = {}")
     case True show ?thesis
     proof (rule_tac f = "\<lambda>x. midpoint a b" in that)
       show "continuous_on U (\<lambda>x. midpoint a b)"
         by (intro continuous_intros)
       show "midpoint a b \<in> closed_segment a b"
         using csegment_midpoint_subset by blast
       show "(midpoint a b = a) = (x \<in> S)" for x
         using \<open>S = {}\<close> \<open>a \<noteq> b\<close> by simp
       show "(midpoint a b = b) = (x \<in> T)" for x
         using \<open>T = {}\<close> \<open>a \<noteq> b\<close> by simp
     qed
   next
     case False
     show ?thesis
     proof (cases "T = U")
       case True with \<open>S = {}\<close> \<open>a \<noteq> b\<close> show ?thesis
         by (rule_tac f = "\<lambda>x. b" in that) (auto)
     next
       case False
       with UT closedin_subset obtain c where c: "c \<in> U" "c \<notin> T"
         by fastforce
       obtain f where f: "continuous_on U f"
                 "\<And>x. x \<in> U \<Longrightarrow> f x \<in> closed_segment (midpoint a b) b"
                 "\<And>x. x \<in> U \<Longrightarrow> (f x = midpoint a b \<longleftrightarrow> x = c)"
                 "\<And>x. x \<in> U \<Longrightarrow> (f x = b \<longleftrightarrow> x \<in> T)"
         apply (rule Urysohn_both_ne [of U "{c}" T "midpoint a b" "b"])
         using c \<open>T \<noteq> {}\<close> assms apply simp_all
         done
       show ?thesis
         apply (rule_tac f=f in that)
         using \<open>S = {}\<close> \<open>T \<noteq> {}\<close> f csegment_midpoint_subset notin_segment_midpoint [OF \<open>a \<noteq> b\<close>]
         apply force+
         done
     qed
   qed
 next
   case False
   show ?thesis
   proof (cases "T = {}")
     case True show ?thesis
     proof (cases "S = U")
       case True with \<open>T = {}\<close> \<open>a \<noteq> b\<close> show ?thesis
         by (rule_tac f = "\<lambda>x. a" in that) (auto)
     next
       case False
       with US closedin_subset obtain c where c: "c \<in> U" "c \<notin> S"
         by fastforce
       obtain f where f: "continuous_on U f"
                 "\<And>x. x \<in> U \<Longrightarrow> f x \<in> closed_segment a (midpoint a b)"
                 "\<And>x. x \<in> U \<Longrightarrow> (f x = midpoint a b \<longleftrightarrow> x = c)"
                 "\<And>x. x \<in> U \<Longrightarrow> (f x = a \<longleftrightarrow> x \<in> S)"
         apply (rule Urysohn_both_ne [of U S "{c}" a "midpoint a b"])
         using c \<open>S \<noteq> {}\<close> assms apply simp_all
         apply (metis midpoint_eq_endpoint)
         done
       show ?thesis
         apply (rule_tac f=f in that)
         using \<open>S \<noteq> {}\<close> \<open>T = {}\<close> f  \<open>a \<noteq> b\<close>
         apply simp_all
         apply (metis (no_types) closed_segment_commute csegment_midpoint_subset midpoint_sym subset_iff)
         apply (metis closed_segment_commute midpoint_sym notin_segment_midpoint)
         done
     qed
   next
     case False
     show ?thesis
       using Urysohn_both_ne [OF US UT \<open>S \<inter> T = {}\<close> \<open>S \<noteq> {}\<close> \<open>T \<noteq> {}\<close> \<open>a \<noteq> b\<close>] that
       by blast
   qed
 qed
 
 lemma Urysohn_local:
   assumes US: "closedin (top_of_set U) S"
       and UT: "closedin (top_of_set U) T"
       and "S \<inter> T = {}"
   obtains f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
     where "continuous_on U f"
           "\<And>x. x \<in> U \<Longrightarrow> f x \<in> closed_segment a b"
           "\<And>x. x \<in> S \<Longrightarrow> f x = a"
           "\<And>x. x \<in> T \<Longrightarrow> f x = b"
 proof (cases "a = b")
   case True then show ?thesis
     by (rule_tac f = "\<lambda>x. b" in that) (auto)
 next
   case False
   then show ?thesis
     apply (rule Urysohn_local_strong [OF assms])
     apply (erule that, assumption)
     apply (meson US closedin_singleton closedin_trans)
     apply (meson UT closedin_singleton closedin_trans)
     done
 qed
 
 lemma Urysohn_strong:
   assumes US: "closed S"
       and UT: "closed T"
       and "S \<inter> T = {}" "a \<noteq> b"
   obtains f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
     where "continuous_on UNIV f"
           "\<And>x. f x \<in> closed_segment a b"
           "\<And>x. f x = a \<longleftrightarrow> x \<in> S"
           "\<And>x. f x = b \<longleftrightarrow> x \<in> T"
 using assms by (auto intro: Urysohn_local_strong [of UNIV S T])
 
 proposition Urysohn:
   assumes US: "closed S"
       and UT: "closed T"
       and "S \<inter> T = {}"
   obtains f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
     where "continuous_on UNIV f"
           "\<And>x. f x \<in> closed_segment a b"
           "\<And>x. x \<in> S \<Longrightarrow> f x = a"
           "\<And>x. x \<in> T \<Longrightarrow> f x = b"
   using assms by (auto intro: Urysohn_local [of UNIV S T a b])
 
 
 subsection\<open>Dugundji's Extension Theorem and Tietze Variants\<close>
 
 text \<open>See \cite{dugundji}.\<close>
 
+lemma convex_supp_sum:
+  assumes "convex S" and 1: "supp_sum u I = 1"
+      and "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> u i \<and> (u i = 0 \<or> f i \<in> S)"
+    shows "supp_sum (\<lambda>i. u i *\<^sub>R f i) I \<in> S"
+proof -
+  have fin: "finite {i \<in> I. u i \<noteq> 0}"
+    using 1 sum.infinite by (force simp: supp_sum_def support_on_def)
+  then have "supp_sum (\<lambda>i. u i *\<^sub>R f i) I = sum (\<lambda>i. u i *\<^sub>R f i) {i \<in> I. u i \<noteq> 0}"
+    by (force intro: sum.mono_neutral_left simp: supp_sum_def support_on_def)
+  also have "... \<in> S"
+    using 1 assms by (force simp: supp_sum_def support_on_def intro: convex_sum [OF fin \<open>convex S\<close>])
+  finally show ?thesis .
+qed
+
 theorem Dugundji:
   fixes f :: "'a::{metric_space,second_countable_topology} \<Rightarrow> 'b::real_inner"
   assumes "convex C" "C \<noteq> {}"
       and cloin: "closedin (top_of_set U) S"
       and contf: "continuous_on S f" and "f ` S \<subseteq> C"
   obtains g where "continuous_on U g" "g ` U \<subseteq> C"
                   "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
 proof (cases "S = {}")
   case True then show thesis
     apply (rule_tac g="\<lambda>x. SOME y. y \<in> C" in that)
       apply (rule continuous_intros)
      apply (meson all_not_in_conv \<open>C \<noteq> {}\<close> image_subsetI someI_ex, simp)
     done
 next
   case False
   then have sd_pos: "\<And>x. \<lbrakk>x \<in> U; x \<notin> S\<rbrakk> \<Longrightarrow> 0 < setdist {x} S"
     using setdist_eq_0_closedin [OF cloin] le_less setdist_pos_le by fastforce
   define \<B> where "\<B> = {ball x (setdist {x} S / 2) |x. x \<in> U - S}"
   have [simp]: "\<And>T. T \<in> \<B> \<Longrightarrow> open T"
     by (auto simp: \<B>_def)
   have USS: "U - S \<subseteq> \<Union>\<B>"
     by (auto simp: sd_pos \<B>_def)
   obtain \<C> where USsub: "U - S \<subseteq> \<Union>\<C>"
        and nbrhd: "\<And>U. U \<in> \<C> \<Longrightarrow> open U \<and> (\<exists>T. T \<in> \<B> \<and> U \<subseteq> T)"
        and fin: "\<And>x. x \<in> U - S \<Longrightarrow> \<exists>V. open V \<and> x \<in> V \<and> finite {U. U \<in> \<C> \<and> U \<inter> V \<noteq> {}}"
     by (rule paracompact [OF USS]) auto
   have "\<exists>v a. v \<in> U \<and> v \<notin> S \<and> a \<in> S \<and>
               T \<subseteq> ball v (setdist {v} S / 2) \<and>
               dist v a \<le> 2 * setdist {v} S" if "T \<in> \<C>" for T
   proof -
     obtain v where v: "T \<subseteq> ball v (setdist {v} S / 2)" "v \<in> U" "v \<notin> S"
       using \<open>T \<in> \<C>\<close> nbrhd by (force simp: \<B>_def)
     then obtain a where "a \<in> S" "dist v a < 2 * setdist {v} S"
       using setdist_ltE [of "{v}" S "2 * setdist {v} S"]
       using False sd_pos by force
     with v show ?thesis
       apply (rule_tac x=v in exI)
       apply (rule_tac x=a in exI, auto)
       done
   qed
   then obtain \<V> \<A> where
     VA: "\<And>T. T \<in> \<C> \<Longrightarrow> \<V> T \<in> U \<and> \<V> T \<notin> S \<and> \<A> T \<in> S \<and>
               T \<subseteq> ball (\<V> T) (setdist {\<V> T} S / 2) \<and>
               dist (\<V> T) (\<A> T) \<le> 2 * setdist {\<V> T} S"
     by metis
   have sdle: "setdist {\<V> T} S \<le> 2 * setdist {v} S" if "T \<in> \<C>" "v \<in> T" for T v
     using setdist_Lipschitz [of "\<V> T" S v] VA [OF \<open>T \<in> \<C>\<close>] \<open>v \<in> T\<close> by auto
   have d6: "dist a (\<A> T) \<le> 6 * dist a v" if "T \<in> \<C>" "v \<in> T" "a \<in> S" for T v a
   proof -
     have "dist (\<V> T) v < setdist {\<V> T} S / 2"
       using that VA mem_ball by blast
     also have "\<dots> \<le> setdist {v} S"
       using sdle [OF \<open>T \<in> \<C>\<close> \<open>v \<in> T\<close>] by simp
     also have vS: "setdist {v} S \<le> dist a v"
       by (simp add: setdist_le_dist setdist_sym \<open>a \<in> S\<close>)
     finally have VTV: "dist (\<V> T) v < dist a v" .
     have VTS: "setdist {\<V> T} S \<le> 2 * dist a v"
       using sdle that vS by force
     have "dist a (\<A> T) \<le> dist a v + dist v (\<V> T) + dist (\<V> T) (\<A> T)"
       by (metis add.commute add_le_cancel_left dist_commute dist_triangle2 dist_triangle_le)
     also have "\<dots> \<le> dist a v + dist a v + dist (\<V> T) (\<A> T)"
       using VTV by (simp add: dist_commute)
     also have "\<dots> \<le> 2 * dist a v + 2 * setdist {\<V> T} S"
       using VA [OF \<open>T \<in> \<C>\<close>] by auto
     finally show ?thesis
       using VTS by linarith
   qed
   obtain H :: "['a set, 'a] \<Rightarrow> real"
     where Hcont: "\<And>Z. Z \<in> \<C> \<Longrightarrow> continuous_on (U-S) (H Z)"
       and Hge0: "\<And>Z x. \<lbrakk>Z \<in> \<C>; x \<in> U-S\<rbrakk> \<Longrightarrow> 0 \<le> H Z x"
       and Heq0: "\<And>x Z. \<lbrakk>Z \<in> \<C>; x \<in> U-S; x \<notin> Z\<rbrakk> \<Longrightarrow> H Z x = 0"
       and H1: "\<And>x. x \<in> U-S \<Longrightarrow> supp_sum (\<lambda>W. H W x) \<C> = 1"
       and Hfin: "\<And>x. x \<in> U-S \<Longrightarrow> \<exists>V. open V \<and> x \<in> V \<and> finite {U \<in> \<C>. \<exists>x\<in>V. H U x \<noteq> 0}"
     apply (rule subordinate_partition_of_unity [OF USsub _ fin])
     using nbrhd by auto
   define g where "g \<equiv> \<lambda>x. if x \<in> S then f x else supp_sum (\<lambda>T. H T x *\<^sub>R f(\<A> T)) \<C>"
   show ?thesis
   proof (rule that)
     show "continuous_on U g"
     proof (clarsimp simp: continuous_on_eq_continuous_within)
       fix a assume "a \<in> U"
       show "continuous (at a within U) g"
       proof (cases "a \<in> S")
         case True show ?thesis
         proof (clarsimp simp add: continuous_within_topological)
           fix W
           assume "open W" "g a \<in> W"
           then obtain e where "0 < e" and e: "ball (f a) e \<subseteq> W"
             using openE True g_def by auto
           have "continuous (at a within S) f"
             using True contf continuous_on_eq_continuous_within by blast
           then obtain d where "0 < d"
                         and d: "\<And>x. \<lbrakk>x \<in> S; dist x a < d\<rbrakk> \<Longrightarrow> dist (f x) (f a) < e"
             using continuous_within_eps_delta \<open>0 < e\<close> by force
           have "g y \<in> ball (f a) e" if "y \<in> U" and y: "y \<in> ball a (d / 6)" for y
           proof (cases "y \<in> S")
             case True
             then have "dist (f a) (f y) < e"
               by (metis ball_divide_subset_numeral dist_commute in_mono mem_ball y d)
             then show ?thesis
               by (simp add: True g_def)
           next
             case False
             have *: "dist (f (\<A> T)) (f a) < e" if "T \<in> \<C>" "H T y \<noteq> 0" for T
             proof -
               have "y \<in> T"
                 using Heq0 that False \<open>y \<in> U\<close> by blast
               have "dist (\<A> T) a < d"
                 using d6 [OF \<open>T \<in> \<C>\<close> \<open>y \<in> T\<close> \<open>a \<in> S\<close>] y
                 by (simp add: dist_commute mult.commute)
               then show ?thesis
                 using VA [OF \<open>T \<in> \<C>\<close>] by (auto simp: d)
             qed
             have "supp_sum (\<lambda>T. H T y *\<^sub>R f (\<A> T)) \<C> \<in> ball (f a) e"
               apply (rule convex_supp_sum [OF convex_ball])
               apply (simp_all add: False H1 Hge0 \<open>y \<in> U\<close>)
               by (metis dist_commute *)
             then show ?thesis
               by (simp add: False g_def)
           qed
           then show "\<exists>A. open A \<and> a \<in> A \<and> (\<forall>y\<in>U. y \<in> A \<longrightarrow> g y \<in> W)"
             apply (rule_tac x = "ball a (d / 6)" in exI)
             using e \<open>0 < d\<close> by fastforce
         qed
       next
         case False
         obtain N where N: "open N" "a \<in> N"
                    and finN: "finite {U \<in> \<C>. \<exists>a\<in>N. H U a \<noteq> 0}"
           using Hfin False \<open>a \<in> U\<close> by auto
         have oUS: "openin (top_of_set U) (U - S)"
           using cloin by (simp add: openin_diff)
         have HcontU: "continuous (at a within U) (H T)" if "T \<in> \<C>" for T
           using Hcont [OF \<open>T \<in> \<C>\<close>] False  \<open>a \<in> U\<close> \<open>T \<in> \<C>\<close>
           apply (simp add: continuous_on_eq_continuous_within continuous_within)
           apply (rule Lim_transform_within_set)
           using oUS
             apply (force simp: eventually_at openin_contains_ball dist_commute dest!: bspec)+
           done
         show ?thesis
         proof (rule continuous_transform_within_openin [OF _ oUS])
           show "continuous (at a within U) (\<lambda>x. supp_sum (\<lambda>T. H T x *\<^sub>R f (\<A> T)) \<C>)"
           proof (rule continuous_transform_within_openin)
             show "continuous (at a within U)
                     (\<lambda>x. \<Sum>T\<in>{U \<in> \<C>. \<exists>x\<in>N. H U x \<noteq> 0}. H T x *\<^sub>R f (\<A> T))"
               by (force intro: continuous_intros HcontU)+
           next
             show "openin (top_of_set U) ((U - S) \<inter> N)"
               using N oUS openin_trans by blast
           next
             show "a \<in> (U - S) \<inter> N" using False \<open>a \<in> U\<close> N by blast
           next
             show "\<And>x. x \<in> (U - S) \<inter> N \<Longrightarrow>
                          (\<Sum>T \<in> {U \<in> \<C>. \<exists>x\<in>N. H U x \<noteq> 0}. H T x *\<^sub>R f (\<A> T))
                          = supp_sum (\<lambda>T. H T x *\<^sub>R f (\<A> T)) \<C>"
               by (auto simp: supp_sum_def support_on_def
                        intro: sum.mono_neutral_right [OF finN])
           qed
         next
           show "a \<in> U - S" using False \<open>a \<in> U\<close> by blast
         next
           show "\<And>x. x \<in> U - S \<Longrightarrow> supp_sum (\<lambda>T. H T x *\<^sub>R f (\<A> T)) \<C> = g x"
             by (simp add: g_def)
         qed
       qed
     qed
     show "g ` U \<subseteq> C"
       using \<open>f ` S \<subseteq> C\<close> VA
       by (fastforce simp: g_def Hge0 intro!: convex_supp_sum [OF \<open>convex C\<close>] H1)
     show "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
       by (simp add: g_def)
   qed
 qed
 
 
 corollary Tietze:
   fixes f :: "'a::{metric_space,second_countable_topology} \<Rightarrow> 'b::real_inner"
   assumes "continuous_on S f"
     and "closedin (top_of_set U) S"
     and "0 \<le> B"
     and "\<And>x. x \<in> S \<Longrightarrow> norm(f x) \<le> B"
   obtains g where "continuous_on U g" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
     "\<And>x. x \<in> U \<Longrightarrow> norm(g x) \<le> B"
   using assms by (auto simp: image_subset_iff intro: Dugundji [of "cball 0 B" U S f])
 
 corollary\<^marker>\<open>tag unimportant\<close> Tietze_closed_interval:
   fixes f :: "'a::{metric_space,second_countable_topology} \<Rightarrow> 'b::euclidean_space"
   assumes "continuous_on S f"
     and "closedin (top_of_set U) S"
     and "cbox a b \<noteq> {}"
     and "\<And>x. x \<in> S \<Longrightarrow> f x \<in> cbox a b"
   obtains g where "continuous_on U g" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
     "\<And>x. x \<in> U \<Longrightarrow> g x \<in> cbox a b"
   apply (rule Dugundji [of "cbox a b" U S f])
   using assms by auto
 
 corollary\<^marker>\<open>tag unimportant\<close> Tietze_closed_interval_1:
   fixes f :: "'a::{metric_space,second_countable_topology} \<Rightarrow> real"
   assumes "continuous_on S f"
     and "closedin (top_of_set U) S"
     and "a \<le> b"
     and "\<And>x. x \<in> S \<Longrightarrow> f x \<in> cbox a b"
   obtains g where "continuous_on U g" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
     "\<And>x. x \<in> U \<Longrightarrow> g x \<in> cbox a b"
   apply (rule Dugundji [of "cbox a b" U S f])
   using assms by (auto simp: image_subset_iff)
 
 corollary\<^marker>\<open>tag unimportant\<close> Tietze_open_interval:
   fixes f :: "'a::{metric_space,second_countable_topology} \<Rightarrow> 'b::euclidean_space"
   assumes "continuous_on S f"
     and "closedin (top_of_set U) S"
     and "box a b \<noteq> {}"
     and "\<And>x. x \<in> S \<Longrightarrow> f x \<in> box a b"
   obtains g where "continuous_on U g" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
     "\<And>x. x \<in> U \<Longrightarrow> g x \<in> box a b"
   apply (rule Dugundji [of "box a b" U S f])
   using assms by auto
 
 corollary\<^marker>\<open>tag unimportant\<close> Tietze_open_interval_1:
   fixes f :: "'a::{metric_space,second_countable_topology} \<Rightarrow> real"
   assumes "continuous_on S f"
     and "closedin (top_of_set U) S"
     and "a < b"
     and no: "\<And>x. x \<in> S \<Longrightarrow> f x \<in> box a b"
   obtains g where "continuous_on U g" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
     "\<And>x. x \<in> U \<Longrightarrow> g x \<in> box a b"
   apply (rule Dugundji [of "box a b" U S f])
   using assms by (auto simp: image_subset_iff)
 
 corollary\<^marker>\<open>tag unimportant\<close> Tietze_unbounded:
   fixes f :: "'a::{metric_space,second_countable_topology} \<Rightarrow> 'b::real_inner"
   assumes "continuous_on S f"
     and "closedin (top_of_set U) S"
   obtains g where "continuous_on U g" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
   apply (rule Dugundji [of UNIV U S f])
   using assms by auto
 
 end
diff --git a/src/HOL/Analysis/Line_Segment.thy b/src/HOL/Analysis/Line_Segment.thy
--- a/src/HOL/Analysis/Line_Segment.thy
+++ b/src/HOL/Analysis/Line_Segment.thy
@@ -1,1265 +1,1195 @@
 (* Title:      HOL/Analysis/Line_Segment.thy
    Author:     L C Paulson, University of Cambridge
    Author:     Robert Himmelmann, TU Muenchen
    Author:     Bogdan Grechuk, University of Edinburgh
    Author:     Armin Heller, TU Muenchen
    Author:     Johannes Hoelzl, TU Muenchen
 *)
 
 section \<open>Line Segment\<close>
 
 theory Line_Segment
 imports
   Convex
   Topology_Euclidean_Space
 begin
 
 subsection\<^marker>\<open>tag unimportant\<close> \<open>Topological Properties of Convex Sets, Metric Spaces and Functions\<close>
 
 lemma convex_supp_sum:
   assumes "convex S" and 1: "supp_sum u I = 1"
       and "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> u i \<and> (u i = 0 \<or> f i \<in> S)"
     shows "supp_sum (\<lambda>i. u i *\<^sub>R f i) I \<in> S"
 proof -
   have fin: "finite {i \<in> I. u i \<noteq> 0}"
     using 1 sum.infinite by (force simp: supp_sum_def support_on_def)
   then have "supp_sum (\<lambda>i. u i *\<^sub>R f i) I = sum (\<lambda>i. u i *\<^sub>R f i) {i \<in> I. u i \<noteq> 0}"
     by (force intro: sum.mono_neutral_left simp: supp_sum_def support_on_def)
   also have "... \<in> S"
     using 1 assms by (force simp: supp_sum_def support_on_def intro: convex_sum [OF fin \<open>convex S\<close>])
   finally show ?thesis .
 qed
 
-lemma closure_bounded_linear_image_subset:
-  assumes f: "bounded_linear f"
-  shows "f ` closure S \<subseteq> closure (f ` S)"
-  using linear_continuous_on [OF f] closed_closure closure_subset
-  by (rule image_closure_subset)
-
-lemma closure_linear_image_subset:
-  fixes f :: "'m::euclidean_space \<Rightarrow> 'n::real_normed_vector"
-  assumes "linear f"
-  shows "f ` (closure S) \<subseteq> closure (f ` S)"
-  using assms unfolding linear_conv_bounded_linear
-  by (rule closure_bounded_linear_image_subset)
-
-lemma closed_injective_linear_image:
-    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
-    assumes S: "closed S" and f: "linear f" "inj f"
-    shows "closed (f ` S)"
-proof -
-  obtain g where g: "linear g" "g \<circ> f = id"
-    using linear_injective_left_inverse [OF f] by blast
-  then have confg: "continuous_on (range f) g"
-    using linear_continuous_on linear_conv_bounded_linear by blast
-  have [simp]: "g ` f ` S = S"
-    using g by (simp add: image_comp)
-  have cgf: "closed (g ` f ` S)"
-    by (simp add: \<open>g \<circ> f = id\<close> S image_comp)
-  have [simp]: "(range f \<inter> g -` S) = f ` S"
-    using g unfolding o_def id_def image_def by auto metis+
-  show ?thesis
-  proof (rule closedin_closed_trans [of "range f"])
-    show "closedin (top_of_set (range f)) (f ` S)"
-      using continuous_closedin_preimage [OF confg cgf] by simp
-    show "closed (range f)"
-      apply (rule closed_injective_image_subspace)
-      using f apply (auto simp: linear_linear linear_injective_0)
-      done
-  qed
-qed
-
-lemma closed_injective_linear_image_eq:
-    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
-    assumes f: "linear f" "inj f"
-      shows "(closed(image f s) \<longleftrightarrow> closed s)"
-  by (metis closed_injective_linear_image closure_eq closure_linear_image_subset closure_subset_eq f(1) f(2) inj_image_subset_iff)
-
-lemma closure_injective_linear_image:
-    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
-    shows "\<lbrakk>linear f; inj f\<rbrakk> \<Longrightarrow> f ` (closure S) = closure (f ` S)"
-  apply (rule subset_antisym)
-  apply (simp add: closure_linear_image_subset)
-  by (simp add: closure_minimal closed_injective_linear_image closure_subset image_mono)
-
-lemma closure_bounded_linear_image:
-    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
-    shows "\<lbrakk>linear f; bounded S\<rbrakk> \<Longrightarrow> f ` (closure S) = closure (f ` S)"
-  apply (rule subset_antisym, simp add: closure_linear_image_subset)
-  apply (rule closure_minimal, simp add: closure_subset image_mono)
-  by (meson bounded_closure closed_closure compact_continuous_image compact_eq_bounded_closed linear_continuous_on linear_conv_bounded_linear)
-
-lemma closure_scaleR:
-  fixes S :: "'a::real_normed_vector set"
-  shows "((*\<^sub>R) c) ` (closure S) = closure (((*\<^sub>R) c) ` S)"
-proof
-  show "((*\<^sub>R) c) ` (closure S) \<subseteq> closure (((*\<^sub>R) c) ` S)"
-    using bounded_linear_scaleR_right
-    by (rule closure_bounded_linear_image_subset)
-  show "closure (((*\<^sub>R) c) ` S) \<subseteq> ((*\<^sub>R) c) ` (closure S)"
-    by (intro closure_minimal image_mono closure_subset closed_scaling closed_closure)
-qed
-
 lemma sphere_eq_empty [simp]:
   fixes a :: "'a::{real_normed_vector, perfect_space}"
   shows "sphere a r = {} \<longleftrightarrow> r < 0"
 by (auto simp: sphere_def dist_norm) (metis dist_norm le_less_linear vector_choose_dist)
 
 lemma cone_closure:
   fixes S :: "'a::real_normed_vector set"
   assumes "cone S"
   shows "cone (closure S)"
 proof (cases "S = {}")
   case True
   then show ?thesis by auto
 next
   case False
   then have "0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> (*\<^sub>R) c ` S = S)"
     using cone_iff[of S] assms by auto
   then have "0 \<in> closure S \<and> (\<forall>c. c > 0 \<longrightarrow> (*\<^sub>R) c ` closure S = closure S)"
     using closure_subset by (auto simp: closure_scaleR)
   then show ?thesis
     using False cone_iff[of "closure S"] by auto
 qed
 
 
 corollary component_complement_connected:
   fixes S :: "'a::real_normed_vector set"
   assumes "connected S" "C \<in> components (-S)"
   shows "connected(-C)"
   using component_diff_connected [of S UNIV] assms
   by (auto simp: Compl_eq_Diff_UNIV)
 
 proposition clopen:
   fixes S :: "'a :: real_normed_vector set"
   shows "closed S \<and> open S \<longleftrightarrow> S = {} \<or> S = UNIV"
   by (force intro!: connected_UNIV [unfolded connected_clopen, rule_format])
 
 corollary compact_open:
   fixes S :: "'a :: euclidean_space set"
   shows "compact S \<and> open S \<longleftrightarrow> S = {}"
   by (auto simp: compact_eq_bounded_closed clopen)
 
 corollary finite_imp_not_open:
   fixes S :: "'a::{real_normed_vector, perfect_space} set"
   shows "\<lbrakk>finite S; open S\<rbrakk> \<Longrightarrow> S={}"
   using clopen [of S] finite_imp_closed not_bounded_UNIV by blast
 
 corollary empty_interior_finite:
     fixes S :: "'a::{real_normed_vector, perfect_space} set"
     shows "finite S \<Longrightarrow> interior S = {}"
   by (metis interior_subset finite_subset open_interior [of S] finite_imp_not_open)
 
 text \<open>Balls, being convex, are connected.\<close>
 
 lemma convex_local_global_minimum:
   fixes s :: "'a::real_normed_vector set"
   assumes "e > 0"
     and "convex_on s f"
     and "ball x e \<subseteq> s"
     and "\<forall>y\<in>ball x e. f x \<le> f y"
   shows "\<forall>y\<in>s. f x \<le> f y"
 proof (rule ccontr)
   have "x \<in> s" using assms(1,3) by auto
   assume "\<not> ?thesis"
   then obtain y where "y\<in>s" and y: "f x > f y" by auto
   then have xy: "0 < dist x y"  by auto
   then obtain u where "0 < u" "u \<le> 1" and u: "u < e / dist x y"
     using field_lbound_gt_zero[of 1 "e / dist x y"] xy \<open>e>0\<close> by auto
   then have "f ((1-u) *\<^sub>R x + u *\<^sub>R y) \<le> (1-u) * f x + u * f y"
     using \<open>x\<in>s\<close> \<open>y\<in>s\<close>
     using assms(2)[unfolded convex_on_def,
       THEN bspec[where x=x], THEN bspec[where x=y], THEN spec[where x="1-u"]]
     by auto
   moreover
   have *: "x - ((1 - u) *\<^sub>R x + u *\<^sub>R y) = u *\<^sub>R (x - y)"
     by (simp add: algebra_simps)
   have "(1 - u) *\<^sub>R x + u *\<^sub>R y \<in> ball x e"
     unfolding mem_ball dist_norm
     unfolding * and norm_scaleR and abs_of_pos[OF \<open>0<u\<close>]
     unfolding dist_norm[symmetric]
     using u
     unfolding pos_less_divide_eq[OF xy]
     by auto
   then have "f x \<le> f ((1 - u) *\<^sub>R x + u *\<^sub>R y)"
     using assms(4) by auto
   ultimately show False
     using mult_strict_left_mono[OF y \<open>u>0\<close>]
     unfolding left_diff_distrib
     by auto
 qed
 
 lemma convex_ball [iff]:
   fixes x :: "'a::real_normed_vector"
   shows "convex (ball x e)"
 proof (auto simp: convex_def)
   fix y z
   assume yz: "dist x y < e" "dist x z < e"
   fix u v :: real
   assume uv: "0 \<le> u" "0 \<le> v" "u + v = 1"
   have "dist x (u *\<^sub>R y + v *\<^sub>R z) \<le> u * dist x y + v * dist x z"
     using uv yz
     using convex_on_dist [of "ball x e" x, unfolded convex_on_def,
       THEN bspec[where x=y], THEN bspec[where x=z]]
     by auto
   then show "dist x (u *\<^sub>R y + v *\<^sub>R z) < e"
     using convex_bound_lt[OF yz uv] by auto
 qed
 
 lemma convex_cball [iff]:
   fixes x :: "'a::real_normed_vector"
   shows "convex (cball x e)"
 proof -
   {
     fix y z
     assume yz: "dist x y \<le> e" "dist x z \<le> e"
     fix u v :: real
     assume uv: "0 \<le> u" "0 \<le> v" "u + v = 1"
     have "dist x (u *\<^sub>R y + v *\<^sub>R z) \<le> u * dist x y + v * dist x z"
       using uv yz
       using convex_on_dist [of "cball x e" x, unfolded convex_on_def,
         THEN bspec[where x=y], THEN bspec[where x=z]]
       by auto
     then have "dist x (u *\<^sub>R y + v *\<^sub>R z) \<le> e"
       using convex_bound_le[OF yz uv] by auto
   }
   then show ?thesis by (auto simp: convex_def Ball_def)
 qed
 
 lemma connected_ball [iff]:
   fixes x :: "'a::real_normed_vector"
   shows "connected (ball x e)"
   using convex_connected convex_ball by auto
 
 lemma connected_cball [iff]:
   fixes x :: "'a::real_normed_vector"
   shows "connected (cball x e)"
   using convex_connected convex_cball by auto
 
 lemma bounded_convex_hull:
   fixes s :: "'a::real_normed_vector set"
   assumes "bounded s"
   shows "bounded (convex hull s)"
 proof -
   from assms obtain B where B: "\<forall>x\<in>s. norm x \<le> B"
     unfolding bounded_iff by auto
   show ?thesis
     by (simp add: bounded_subset[OF bounded_cball, of _ 0 B] B subsetI subset_hull)
 qed
 
 lemma finite_imp_bounded_convex_hull:
   fixes s :: "'a::real_normed_vector set"
   shows "finite s \<Longrightarrow> bounded (convex hull s)"
   using bounded_convex_hull finite_imp_bounded
   by auto
 
 
 subsection \<open>Midpoint\<close>
 
 definition\<^marker>\<open>tag important\<close> midpoint :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a"
   where "midpoint a b = (inverse (2::real)) *\<^sub>R (a + b)"
 
 lemma midpoint_idem [simp]: "midpoint x x = x"
   unfolding midpoint_def  by simp
 
 lemma midpoint_sym: "midpoint a b = midpoint b a"
   unfolding midpoint_def by (auto simp add: scaleR_right_distrib)
 
 lemma midpoint_eq_iff: "midpoint a b = c \<longleftrightarrow> a + b = c + c"
 proof -
   have "midpoint a b = c \<longleftrightarrow> scaleR 2 (midpoint a b) = scaleR 2 c"
     by simp
   then show ?thesis
     unfolding midpoint_def scaleR_2 [symmetric] by simp
 qed
 
 lemma
   fixes a::real
   assumes "a \<le> b" shows ge_midpoint_1: "a \<le> midpoint a b"
                     and le_midpoint_1: "midpoint a b \<le> b"
   by (simp_all add: midpoint_def assms)
 
 lemma dist_midpoint:
   fixes a b :: "'a::real_normed_vector" shows
   "dist a (midpoint a b) = (dist a b) / 2" (is ?t1)
   "dist b (midpoint a b) = (dist a b) / 2" (is ?t2)
   "dist (midpoint a b) a = (dist a b) / 2" (is ?t3)
   "dist (midpoint a b) b = (dist a b) / 2" (is ?t4)
 proof -
   have *: "\<And>x y::'a. 2 *\<^sub>R x = - y \<Longrightarrow> norm x = (norm y) / 2"
     unfolding equation_minus_iff by auto
   have **: "\<And>x y::'a. 2 *\<^sub>R x =   y \<Longrightarrow> norm x = (norm y) / 2"
     by auto
   note scaleR_right_distrib [simp]
   show ?t1
     unfolding midpoint_def dist_norm
     apply (rule **)
     apply (simp add: scaleR_right_diff_distrib)
     apply (simp add: scaleR_2)
     done
   show ?t2
     unfolding midpoint_def dist_norm
     apply (rule *)
     apply (simp add: scaleR_right_diff_distrib)
     apply (simp add: scaleR_2)
     done
   show ?t3
     unfolding midpoint_def dist_norm
     apply (rule *)
     apply (simp add: scaleR_right_diff_distrib)
     apply (simp add: scaleR_2)
     done
   show ?t4
     unfolding midpoint_def dist_norm
     apply (rule **)
     apply (simp add: scaleR_right_diff_distrib)
     apply (simp add: scaleR_2)
     done
 qed
 
 lemma midpoint_eq_endpoint [simp]:
   "midpoint a b = a \<longleftrightarrow> a = b"
   "midpoint a b = b \<longleftrightarrow> a = b"
   unfolding midpoint_eq_iff by auto
 
 lemma midpoint_plus_self [simp]: "midpoint a b + midpoint a b = a + b"
   using midpoint_eq_iff by metis
 
 lemma midpoint_linear_image:
    "linear f \<Longrightarrow> midpoint(f a)(f b) = f(midpoint a b)"
 by (simp add: linear_iff midpoint_def)
 
 
 subsection \<open>Open and closed segments\<close>
 
 definition\<^marker>\<open>tag important\<close> closed_segment :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a set"
   where "closed_segment a b = {(1 - u) *\<^sub>R a + u *\<^sub>R b | u::real. 0 \<le> u \<and> u \<le> 1}"
 
 definition\<^marker>\<open>tag important\<close> open_segment :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a set" where
   "open_segment a b \<equiv> closed_segment a b - {a,b}"
 
 lemmas segment = open_segment_def closed_segment_def
 
 lemma in_segment:
     "x \<in> closed_segment a b \<longleftrightarrow> (\<exists>u. 0 \<le> u \<and> u \<le> 1 \<and> x = (1 - u) *\<^sub>R a + u *\<^sub>R b)"
     "x \<in> open_segment a b \<longleftrightarrow> a \<noteq> b \<and> (\<exists>u. 0 < u \<and> u < 1 \<and> x = (1 - u) *\<^sub>R a + u *\<^sub>R b)"
   using less_eq_real_def by (auto simp: segment algebra_simps)
 
 lemma closed_segment_linear_image:
   "closed_segment (f a) (f b) = f ` (closed_segment a b)" if "linear f"
 proof -
   interpret linear f by fact
   show ?thesis
     by (force simp add: in_segment add scale)
 qed
 
 lemma open_segment_linear_image:
     "\<lbrakk>linear f; inj f\<rbrakk> \<Longrightarrow> open_segment (f a) (f b) = f ` (open_segment a b)"
   by (force simp: open_segment_def closed_segment_linear_image inj_on_def)
 
 lemma closed_segment_translation:
     "closed_segment (c + a) (c + b) = image (\<lambda>x. c + x) (closed_segment a b)"
 apply safe
 apply (rule_tac x="x-c" in image_eqI)
 apply (auto simp: in_segment algebra_simps)
 done
 
 lemma open_segment_translation:
     "open_segment (c + a) (c + b) = image (\<lambda>x. c + x) (open_segment a b)"
 by (simp add: open_segment_def closed_segment_translation translation_diff)
 
 lemma closed_segment_of_real:
     "closed_segment (of_real x) (of_real y) = of_real ` closed_segment x y"
   apply (auto simp: image_iff in_segment scaleR_conv_of_real)
     apply (rule_tac x="(1-u)*x + u*y" in bexI)
   apply (auto simp: in_segment)
   done
 
 lemma open_segment_of_real:
     "open_segment (of_real x) (of_real y) = of_real ` open_segment x y"
   apply (auto simp: image_iff in_segment scaleR_conv_of_real)
     apply (rule_tac x="(1-u)*x + u*y" in bexI)
   apply (auto simp: in_segment)
   done
 
 lemma closed_segment_Reals:
     "\<lbrakk>x \<in> Reals; y \<in> Reals\<rbrakk> \<Longrightarrow> closed_segment x y = of_real ` closed_segment (Re x) (Re y)"
   by (metis closed_segment_of_real of_real_Re)
 
 lemma open_segment_Reals:
     "\<lbrakk>x \<in> Reals; y \<in> Reals\<rbrakk> \<Longrightarrow> open_segment x y = of_real ` open_segment (Re x) (Re y)"
   by (metis open_segment_of_real of_real_Re)
 
 lemma open_segment_PairD:
     "(x, x') \<in> open_segment (a, a') (b, b')
      \<Longrightarrow> (x \<in> open_segment a b \<or> a = b) \<and> (x' \<in> open_segment a' b' \<or> a' = b')"
   by (auto simp: in_segment)
 
 lemma closed_segment_PairD:
   "(x, x') \<in> closed_segment (a, a') (b, b') \<Longrightarrow> x \<in> closed_segment a b \<and> x' \<in> closed_segment a' b'"
   by (auto simp: closed_segment_def)
 
 lemma closed_segment_translation_eq [simp]:
     "d + x \<in> closed_segment (d + a) (d + b) \<longleftrightarrow> x \<in> closed_segment a b"
 proof -
   have *: "\<And>d x a b. x \<in> closed_segment a b \<Longrightarrow> d + x \<in> closed_segment (d + a) (d + b)"
     apply (simp add: closed_segment_def)
     apply (erule ex_forward)
     apply (simp add: algebra_simps)
     done
   show ?thesis
   using * [where d = "-d"] *
   by (fastforce simp add:)
 qed
 
 lemma open_segment_translation_eq [simp]:
     "d + x \<in> open_segment (d + a) (d + b) \<longleftrightarrow> x \<in> open_segment a b"
   by (simp add: open_segment_def)
 
 lemma of_real_closed_segment [simp]:
   "of_real x \<in> closed_segment (of_real a) (of_real b) \<longleftrightarrow> x \<in> closed_segment a b"
   apply (auto simp: in_segment scaleR_conv_of_real elim!: ex_forward)
   using of_real_eq_iff by fastforce
 
 lemma of_real_open_segment [simp]:
   "of_real x \<in> open_segment (of_real a) (of_real b) \<longleftrightarrow> x \<in> open_segment a b"
   apply (auto simp: in_segment scaleR_conv_of_real elim!: ex_forward del: exE)
   using of_real_eq_iff by fastforce
 
 lemma convex_contains_segment:
   "convex S \<longleftrightarrow> (\<forall>a\<in>S. \<forall>b\<in>S. closed_segment a b \<subseteq> S)"
   unfolding convex_alt closed_segment_def by auto
 
 lemma closed_segment_in_Reals:
    "\<lbrakk>x \<in> closed_segment a b; a \<in> Reals; b \<in> Reals\<rbrakk> \<Longrightarrow> x \<in> Reals"
   by (meson subsetD convex_Reals convex_contains_segment)
 
 lemma open_segment_in_Reals:
    "\<lbrakk>x \<in> open_segment a b; a \<in> Reals; b \<in> Reals\<rbrakk> \<Longrightarrow> x \<in> Reals"
   by (metis Diff_iff closed_segment_in_Reals open_segment_def)
 
 lemma closed_segment_subset: "\<lbrakk>x \<in> S; y \<in> S; convex S\<rbrakk> \<Longrightarrow> closed_segment x y \<subseteq> S"
   by (simp add: convex_contains_segment)
 
 lemma closed_segment_subset_convex_hull:
     "\<lbrakk>x \<in> convex hull S; y \<in> convex hull S\<rbrakk> \<Longrightarrow> closed_segment x y \<subseteq> convex hull S"
   using convex_contains_segment by blast
 
 lemma segment_convex_hull:
   "closed_segment a b = convex hull {a,b}"
 proof -
   have *: "\<And>x. {x} \<noteq> {}" by auto
   show ?thesis
     unfolding segment convex_hull_insert[OF *] convex_hull_singleton
     by (safe; rule_tac x="1 - u" in exI; force)
 qed
 
 lemma open_closed_segment: "u \<in> open_segment w z \<Longrightarrow> u \<in> closed_segment w z"
   by (auto simp add: closed_segment_def open_segment_def)
 
 lemma segment_open_subset_closed:
    "open_segment a b \<subseteq> closed_segment a b"
   by (auto simp: closed_segment_def open_segment_def)
 
 lemma bounded_closed_segment:
   fixes a :: "'a::real_normed_vector" shows "bounded (closed_segment a b)"
   by (rule boundedI[where B="max (norm a) (norm b)"])
     (auto simp: closed_segment_def max_def convex_bound_le intro!: norm_triangle_le)
 
 lemma bounded_open_segment:
     fixes a :: "'a::real_normed_vector" shows "bounded (open_segment a b)"
   by (rule bounded_subset [OF bounded_closed_segment segment_open_subset_closed])
 
 lemmas bounded_segment = bounded_closed_segment open_closed_segment
 
 lemma ends_in_segment [iff]: "a \<in> closed_segment a b" "b \<in> closed_segment a b"
   unfolding segment_convex_hull
   by (auto intro!: hull_subset[unfolded subset_eq, rule_format])
 
 
 lemma eventually_closed_segment:
   fixes x0::"'a::real_normed_vector"
   assumes "open X0" "x0 \<in> X0"
   shows "\<forall>\<^sub>F x in at x0 within U. closed_segment x0 x \<subseteq> X0"
 proof -
   from openE[OF assms]
   obtain e where e: "0 < e" "ball x0 e \<subseteq> X0" .
   then have "\<forall>\<^sub>F x in at x0 within U. x \<in> ball x0 e"
     by (auto simp: dist_commute eventually_at)
   then show ?thesis
   proof eventually_elim
     case (elim x)
     have "x0 \<in> ball x0 e" using \<open>e > 0\<close> by simp
     from convex_ball[unfolded convex_contains_segment, rule_format, OF this elim]
     have "closed_segment x0 x \<subseteq> ball x0 e" .
     also note \<open>\<dots> \<subseteq> X0\<close>
     finally show ?case .
   qed
 qed
 
 lemma closed_segment_commute: "closed_segment a b = closed_segment b a"
 proof -
   have "{a, b} = {b, a}" by auto
   thus ?thesis
     by (simp add: segment_convex_hull)
 qed
 
 lemma segment_bound1:
   assumes "x \<in> closed_segment a b"
   shows "norm (x - a) \<le> norm (b - a)"
 proof -
   obtain u where "x = (1 - u) *\<^sub>R a + u *\<^sub>R b" "0 \<le> u" "u \<le> 1"
     using assms by (auto simp add: closed_segment_def)
   then show "norm (x - a) \<le> norm (b - a)"
     apply clarify
     apply (auto simp: algebra_simps)
     apply (simp add: scaleR_diff_right [symmetric] mult_left_le_one_le)
     done
 qed
 
 lemma segment_bound:
   assumes "x \<in> closed_segment a b"
   shows "norm (x - a) \<le> norm (b - a)" "norm (x - b) \<le> norm (b - a)"
 by (metis assms closed_segment_commute dist_commute dist_norm segment_bound1)+
 
 lemma open_segment_commute: "open_segment a b = open_segment b a"
 proof -
   have "{a, b} = {b, a}" by auto
   thus ?thesis
     by (simp add: closed_segment_commute open_segment_def)
 qed
 
 lemma closed_segment_idem [simp]: "closed_segment a a = {a}"
   unfolding segment by (auto simp add: algebra_simps)
 
 lemma open_segment_idem [simp]: "open_segment a a = {}"
   by (simp add: open_segment_def)
 
 lemma closed_segment_eq_open: "closed_segment a b = open_segment a b \<union> {a,b}"
   using open_segment_def by auto
 
 lemma convex_contains_open_segment:
   "convex s \<longleftrightarrow> (\<forall>a\<in>s. \<forall>b\<in>s. open_segment a b \<subseteq> s)"
   by (simp add: convex_contains_segment closed_segment_eq_open)
 
 lemma closed_segment_eq_real_ivl1:
   fixes a b::real
   assumes "a \<le> b"
   shows "closed_segment a b = {a .. b}"
 proof safe
   fix x
   assume "x \<in> closed_segment a b"
   then obtain u where u: "0 \<le> u" "u \<le> 1" and x_def: "x = (1 - u) * a + u * b"
     by (auto simp: closed_segment_def)
   have "u * a \<le> u * b" "(1 - u) * a \<le> (1 - u) * b"
     by (auto intro!: mult_left_mono u assms)
   then show "x \<in> {a .. b}"
     unfolding x_def by (auto simp: algebra_simps)
 next
   show "\<And>x. x \<in> {a..b} \<Longrightarrow> x \<in> closed_segment a b"
     by (force simp: closed_segment_def divide_simps algebra_simps
               intro: exI[where x="(x - a) / (b - a)" for x])
 qed 
 
 lemma closed_segment_eq_real_ivl:
   fixes a b::real
   shows "closed_segment a b = (if a \<le> b then {a .. b} else {b .. a})"
   using closed_segment_eq_real_ivl1[of a b] closed_segment_eq_real_ivl1[of b a]
   by (auto simp: closed_segment_commute)
 
 lemma open_segment_eq_real_ivl:
   fixes a b::real
   shows "open_segment a b = (if a \<le> b then {a<..<b} else {b<..<a})"
 by (auto simp: closed_segment_eq_real_ivl open_segment_def split: if_split_asm)
 
 lemma closed_segment_real_eq:
   fixes u::real shows "closed_segment u v = (\<lambda>x. (v - u) * x + u) ` {0..1}"
   by (simp add: add.commute [of u] image_affinity_atLeastAtMost [where c=u] closed_segment_eq_real_ivl)
 
 lemma closed_segment_same_Re:
   assumes "Re a = Re b"
   shows   "closed_segment a b = {z. Re z = Re a \<and> Im z \<in> closed_segment (Im a) (Im b)}"
 proof safe
   fix z assume "z \<in> closed_segment a b"
   then obtain u where u: "u \<in> {0..1}" "z = a + of_real u * (b - a)"
     by (auto simp: closed_segment_def scaleR_conv_of_real algebra_simps)
   from assms show "Re z = Re a" by (auto simp: u)
   from u(1) show "Im z \<in> closed_segment (Im a) (Im b)"
     by (force simp: u closed_segment_def algebra_simps)
 next
   fix z assume [simp]: "Re z = Re a" and "Im z \<in> closed_segment (Im a) (Im b)"
   then obtain u where u: "u \<in> {0..1}" "Im z = Im a + of_real u * (Im b - Im a)"
     by (auto simp: closed_segment_def scaleR_conv_of_real algebra_simps)
   from u(1) show "z \<in> closed_segment a b" using assms
     by (force simp: u closed_segment_def algebra_simps scaleR_conv_of_real complex_eq_iff)
 qed
 
 lemma closed_segment_same_Im:
   assumes "Im a = Im b"
   shows   "closed_segment a b = {z. Im z = Im a \<and> Re z \<in> closed_segment (Re a) (Re b)}"
 proof safe
   fix z assume "z \<in> closed_segment a b"
   then obtain u where u: "u \<in> {0..1}" "z = a + of_real u * (b - a)"
     by (auto simp: closed_segment_def scaleR_conv_of_real algebra_simps)
   from assms show "Im z = Im a" by (auto simp: u)
   from u(1) show "Re z \<in> closed_segment (Re a) (Re b)"
     by (force simp: u closed_segment_def algebra_simps)
 next
   fix z assume [simp]: "Im z = Im a" and "Re z \<in> closed_segment (Re a) (Re b)"
   then obtain u where u: "u \<in> {0..1}" "Re z = Re a + of_real u * (Re b - Re a)"
     by (auto simp: closed_segment_def scaleR_conv_of_real algebra_simps)
   from u(1) show "z \<in> closed_segment a b" using assms
     by (force simp: u closed_segment_def algebra_simps scaleR_conv_of_real complex_eq_iff)
 qed
 
 lemma dist_in_closed_segment:
   fixes a :: "'a :: euclidean_space"
   assumes "x \<in> closed_segment a b"
     shows "dist x a \<le> dist a b \<and> dist x b \<le> dist a b"
 proof (intro conjI)
   obtain u where u: "0 \<le> u" "u \<le> 1" and x: "x = (1 - u) *\<^sub>R a + u *\<^sub>R b"
     using assms by (force simp: in_segment algebra_simps)
   have "dist x a = u * dist a b"
     apply (simp add: dist_norm algebra_simps x)
     by (metis \<open>0 \<le> u\<close> abs_of_nonneg norm_minus_commute norm_scaleR real_vector.scale_right_diff_distrib)
   also have "...  \<le> dist a b"
     by (simp add: mult_left_le_one_le u)
   finally show "dist x a \<le> dist a b" .
   have "dist x b = norm ((1-u) *\<^sub>R a - (1-u) *\<^sub>R b)"
     by (simp add: dist_norm algebra_simps x)
   also have "... = (1-u) * dist a b"
   proof -
     have "norm ((1 - 1 * u) *\<^sub>R (a - b)) = (1 - 1 * u) * norm (a - b)"
       using \<open>u \<le> 1\<close> by force
     then show ?thesis
       by (simp add: dist_norm real_vector.scale_right_diff_distrib)
   qed
   also have "... \<le> dist a b"
     by (simp add: mult_left_le_one_le u)
   finally show "dist x b \<le> dist a b" .
 qed
 
 lemma dist_in_open_segment:
   fixes a :: "'a :: euclidean_space"
   assumes "x \<in> open_segment a b"
     shows "dist x a < dist a b \<and> dist x b < dist a b"
 proof (intro conjI)
   obtain u where u: "0 < u" "u < 1" and x: "x = (1 - u) *\<^sub>R a + u *\<^sub>R b"
     using assms by (force simp: in_segment algebra_simps)
   have "dist x a = u * dist a b"
     apply (simp add: dist_norm algebra_simps x)
     by (metis abs_of_nonneg less_eq_real_def norm_minus_commute norm_scaleR real_vector.scale_right_diff_distrib \<open>0 < u\<close>)
   also have *: "...  < dist a b"
     by (metis (no_types) assms dist_eq_0_iff dist_not_less_zero in_segment(2) linorder_neqE_linordered_idom mult.left_neutral real_mult_less_iff1 \<open>u < 1\<close>)
   finally show "dist x a < dist a b" .
   have ab_ne0: "dist a b \<noteq> 0"
     using * by fastforce
   have "dist x b = norm ((1-u) *\<^sub>R a - (1-u) *\<^sub>R b)"
     by (simp add: dist_norm algebra_simps x)
   also have "... = (1-u) * dist a b"
   proof -
     have "norm ((1 - 1 * u) *\<^sub>R (a - b)) = (1 - 1 * u) * norm (a - b)"
       using \<open>u < 1\<close> by force
     then show ?thesis
       by (simp add: dist_norm real_vector.scale_right_diff_distrib)
   qed
   also have "... < dist a b"
     using ab_ne0 \<open>0 < u\<close> by simp
   finally show "dist x b < dist a b" .
 qed
 
 lemma dist_decreases_open_segment_0:
   fixes x :: "'a :: euclidean_space"
   assumes "x \<in> open_segment 0 b"
     shows "dist c x < dist c 0 \<or> dist c x < dist c b"
 proof (rule ccontr, clarsimp simp: not_less)
   obtain u where u: "0 \<noteq> b" "0 < u" "u < 1" and x: "x = u *\<^sub>R b"
     using assms by (auto simp: in_segment)
   have xb: "x \<bullet> b < b \<bullet> b"
     using u x by auto
   assume "norm c \<le> dist c x"
   then have "c \<bullet> c \<le> (c - x) \<bullet> (c - x)"
     by (simp add: dist_norm norm_le)
   moreover have "0 < x \<bullet> b"
     using u x by auto
   ultimately have less: "c \<bullet> b < x \<bullet> b"
     by (simp add: x algebra_simps inner_commute u)
   assume "dist c b \<le> dist c x"
   then have "(c - b) \<bullet> (c - b) \<le> (c - x) \<bullet> (c - x)"
     by (simp add: dist_norm norm_le)
   then have "(b \<bullet> b) * (1 - u*u) \<le> 2 * (b \<bullet> c) * (1-u)"
     by (simp add: x algebra_simps inner_commute)
   then have "(1+u) * (b \<bullet> b) * (1-u) \<le> 2 * (b \<bullet> c) * (1-u)"
     by (simp add: algebra_simps)
   then have "(1+u) * (b \<bullet> b) \<le> 2 * (b \<bullet> c)"
     using \<open>u < 1\<close> by auto
   with xb have "c \<bullet> b \<ge> x \<bullet> b"
     by (auto simp: x algebra_simps inner_commute)
   with less show False by auto
 qed
 
 proposition dist_decreases_open_segment:
   fixes a :: "'a :: euclidean_space"
   assumes "x \<in> open_segment a b"
     shows "dist c x < dist c a \<or> dist c x < dist c b"
 proof -
   have *: "x - a \<in> open_segment 0 (b - a)" using assms
     by (metis diff_self open_segment_translation_eq uminus_add_conv_diff)
   show ?thesis
     using dist_decreases_open_segment_0 [OF *, of "c-a"] assms
     by (simp add: dist_norm)
 qed
 
 corollary open_segment_furthest_le:
   fixes a b x y :: "'a::euclidean_space"
   assumes "x \<in> open_segment a b"
   shows "norm (y - x) < norm (y - a) \<or>  norm (y - x) < norm (y - b)"
   by (metis assms dist_decreases_open_segment dist_norm)
 
 corollary dist_decreases_closed_segment:
   fixes a :: "'a :: euclidean_space"
   assumes "x \<in> closed_segment a b"
     shows "dist c x \<le> dist c a \<or> dist c x \<le> dist c b"
 apply (cases "x \<in> open_segment a b")
  using dist_decreases_open_segment less_eq_real_def apply blast
 by (metis DiffI assms empty_iff insertE open_segment_def order_refl)
 
 corollary segment_furthest_le:
   fixes a b x y :: "'a::euclidean_space"
   assumes "x \<in> closed_segment a b"
   shows "norm (y - x) \<le> norm (y - a) \<or>  norm (y - x) \<le> norm (y - b)"
   by (metis assms dist_decreases_closed_segment dist_norm)
 
 lemma convex_intermediate_ball:
   fixes a :: "'a :: euclidean_space"
   shows "\<lbrakk>ball a r \<subseteq> T; T \<subseteq> cball a r\<rbrakk> \<Longrightarrow> convex T"
 apply (simp add: convex_contains_open_segment, clarify)
 by (metis (no_types, hide_lams) less_le_trans mem_ball mem_cball subsetCE dist_decreases_open_segment)
 
 lemma csegment_midpoint_subset: "closed_segment (midpoint a b) b \<subseteq> closed_segment a b"
   apply (clarsimp simp: midpoint_def in_segment)
   apply (rule_tac x="(1 + u) / 2" in exI)
   apply (auto simp: algebra_simps add_divide_distrib diff_divide_distrib)
   by (metis field_sum_of_halves scaleR_left.add)
 
 lemma notin_segment_midpoint:
   fixes a :: "'a :: euclidean_space"
   shows "a \<noteq> b \<Longrightarrow> a \<notin> closed_segment (midpoint a b) b"
 by (auto simp: dist_midpoint dest!: dist_in_closed_segment)
 
 subsubsection\<open>More lemmas, especially for working with the underlying formula\<close>
 
 lemma segment_eq_compose:
   fixes a :: "'a :: real_vector"
   shows "(\<lambda>u. (1 - u) *\<^sub>R a + u *\<^sub>R b) = (\<lambda>x. a + x) o (\<lambda>u. u *\<^sub>R (b - a))"
     by (simp add: o_def algebra_simps)
 
 lemma segment_degen_1:
   fixes a :: "'a :: real_vector"
   shows "(1 - u) *\<^sub>R a + u *\<^sub>R b = b \<longleftrightarrow> a=b \<or> u=1"
 proof -
   { assume "(1 - u) *\<^sub>R a + u *\<^sub>R b = b"
     then have "(1 - u) *\<^sub>R a = (1 - u) *\<^sub>R b"
       by (simp add: algebra_simps)
     then have "a=b \<or> u=1"
       by simp
   } then show ?thesis
       by (auto simp: algebra_simps)
 qed
 
 lemma segment_degen_0:
     fixes a :: "'a :: real_vector"
     shows "(1 - u) *\<^sub>R a + u *\<^sub>R b = a \<longleftrightarrow> a=b \<or> u=0"
   using segment_degen_1 [of "1-u" b a]
   by (auto simp: algebra_simps)
 
 lemma add_scaleR_degen:
   fixes a b ::"'a::real_vector"
   assumes  "(u *\<^sub>R b + v *\<^sub>R a) = (u *\<^sub>R a + v *\<^sub>R b)"  "u \<noteq> v"
   shows "a=b"
   by (metis (no_types, hide_lams) add.commute add_diff_eq diff_add_cancel real_vector.scale_cancel_left real_vector.scale_left_diff_distrib assms)
   
 lemma closed_segment_image_interval:
      "closed_segment a b = (\<lambda>u. (1 - u) *\<^sub>R a + u *\<^sub>R b) ` {0..1}"
   by (auto simp: set_eq_iff image_iff closed_segment_def)
 
 lemma open_segment_image_interval:
      "open_segment a b = (if a=b then {} else (\<lambda>u. (1 - u) *\<^sub>R a + u *\<^sub>R b) ` {0<..<1})"
   by (auto simp:  open_segment_def closed_segment_def segment_degen_0 segment_degen_1)
 
 lemmas segment_image_interval = closed_segment_image_interval open_segment_image_interval
 
 lemma closed_segment_neq_empty [simp]: "closed_segment a b \<noteq> {}"
   by auto
 
 lemma open_segment_eq_empty [simp]: "open_segment a b = {} \<longleftrightarrow> a = b"
 proof -
   { assume a1: "open_segment a b = {}"
     have "{} \<noteq> {0::real<..<1}"
       by simp
     then have "a = b"
       using a1 open_segment_image_interval by fastforce
   } then show ?thesis by auto
 qed
 
 lemma open_segment_eq_empty' [simp]: "{} = open_segment a b \<longleftrightarrow> a = b"
   using open_segment_eq_empty by blast
 
 lemmas segment_eq_empty = closed_segment_neq_empty open_segment_eq_empty
 
 lemma inj_segment:
   fixes a :: "'a :: real_vector"
   assumes "a \<noteq> b"
     shows "inj_on (\<lambda>u. (1 - u) *\<^sub>R a + u *\<^sub>R b) I"
 proof
   fix x y
   assume "(1 - x) *\<^sub>R a + x *\<^sub>R b = (1 - y) *\<^sub>R a + y *\<^sub>R b"
   then have "x *\<^sub>R (b - a) = y *\<^sub>R (b - a)"
     by (simp add: algebra_simps)
   with assms show "x = y"
     by (simp add: real_vector.scale_right_imp_eq)
 qed
 
 lemma finite_closed_segment [simp]: "finite(closed_segment a b) \<longleftrightarrow> a = b"
   apply auto
   apply (rule ccontr)
   apply (simp add: segment_image_interval)
   using infinite_Icc [OF zero_less_one] finite_imageD [OF _ inj_segment] apply blast
   done
 
 lemma finite_open_segment [simp]: "finite(open_segment a b) \<longleftrightarrow> a = b"
   by (auto simp: open_segment_def)
 
 lemmas finite_segment = finite_closed_segment finite_open_segment
 
 lemma closed_segment_eq_sing: "closed_segment a b = {c} \<longleftrightarrow> a = c \<and> b = c"
   by auto
 
 lemma open_segment_eq_sing: "open_segment a b \<noteq> {c}"
   by (metis finite_insert finite_open_segment insert_not_empty open_segment_image_interval)
 
 lemmas segment_eq_sing = closed_segment_eq_sing open_segment_eq_sing
 
 lemma open_segment_bound1:
   assumes "x \<in> open_segment a b"
   shows "norm (x - a) < norm (b - a)"
 proof -
   obtain u where "x = (1 - u) *\<^sub>R a + u *\<^sub>R b" "0 < u" "u < 1" "a \<noteq> b"
     using assms by (auto simp add: open_segment_image_interval split: if_split_asm)
   then show "norm (x - a) < norm (b - a)"
     apply clarify
     apply (auto simp: algebra_simps)
     apply (simp add: scaleR_diff_right [symmetric])
     done
 qed
 
 lemma compact_segment [simp]:
   fixes a :: "'a::real_normed_vector"
   shows "compact (closed_segment a b)"
   by (auto simp: segment_image_interval intro!: compact_continuous_image continuous_intros)
 
 lemma closed_segment [simp]:
   fixes a :: "'a::real_normed_vector"
   shows "closed (closed_segment a b)"
   by (simp add: compact_imp_closed)
 
 lemma closure_closed_segment [simp]:
   fixes a :: "'a::real_normed_vector"
   shows "closure(closed_segment a b) = closed_segment a b"
   by simp
 
 lemma open_segment_bound:
   assumes "x \<in> open_segment a b"
   shows "norm (x - a) < norm (b - a)" "norm (x - b) < norm (b - a)"
 apply (simp add: assms open_segment_bound1)
 by (metis assms norm_minus_commute open_segment_bound1 open_segment_commute)
 
 lemma closure_open_segment [simp]:
   "closure (open_segment a b) = (if a = b then {} else closed_segment a b)"
     for a :: "'a::euclidean_space"
 proof (cases "a = b")
   case True
   then show ?thesis
     by simp
 next
   case False
   have "closure ((\<lambda>u. u *\<^sub>R (b - a)) ` {0<..<1}) = (\<lambda>u. u *\<^sub>R (b - a)) ` closure {0<..<1}"
     apply (rule closure_injective_linear_image [symmetric])
      apply (use False in \<open>auto intro!: injI\<close>)
     done
   then have "closure
      ((\<lambda>u. (1 - u) *\<^sub>R a + u *\<^sub>R b) ` {0<..<1}) =
     (\<lambda>x. (1 - x) *\<^sub>R a + x *\<^sub>R b) ` closure {0<..<1}"
     using closure_translation [of a "((\<lambda>x. x *\<^sub>R b - x *\<^sub>R a) ` {0<..<1})"]
     by (simp add: segment_eq_compose field_simps scaleR_diff_left scaleR_diff_right image_image)
   then show ?thesis
     by (simp add: segment_image_interval closure_greaterThanLessThan [symmetric] del: closure_greaterThanLessThan)
 qed
 
 lemma closed_open_segment_iff [simp]:
     fixes a :: "'a::euclidean_space"  shows "closed(open_segment a b) \<longleftrightarrow> a = b"
   by (metis open_segment_def DiffE closure_eq closure_open_segment ends_in_segment(1) insert_iff segment_image_interval(2))
 
 lemma compact_open_segment_iff [simp]:
     fixes a :: "'a::euclidean_space"  shows "compact(open_segment a b) \<longleftrightarrow> a = b"
   by (simp add: bounded_open_segment compact_eq_bounded_closed)
 
 lemma convex_closed_segment [iff]: "convex (closed_segment a b)"
   unfolding segment_convex_hull by(rule convex_convex_hull)
 
 lemma convex_open_segment [iff]: "convex (open_segment a b)"
 proof -
   have "convex ((\<lambda>u. u *\<^sub>R (b - a)) ` {0<..<1})"
     by (rule convex_linear_image) auto
   then have "convex ((+) a ` (\<lambda>u. u *\<^sub>R (b - a)) ` {0<..<1})"
     by (rule convex_translation)
   then show ?thesis
     by (simp add: image_image open_segment_image_interval segment_eq_compose field_simps scaleR_diff_left scaleR_diff_right)
 qed
 
 lemmas convex_segment = convex_closed_segment convex_open_segment
 
 lemma subset_closed_segment:
     "closed_segment a b \<subseteq> closed_segment c d \<longleftrightarrow>
      a \<in> closed_segment c d \<and> b \<in> closed_segment c d"
   by auto (meson contra_subsetD convex_closed_segment convex_contains_segment)
 
 lemma subset_co_segment:
     "closed_segment a b \<subseteq> open_segment c d \<longleftrightarrow>
      a \<in> open_segment c d \<and> b \<in> open_segment c d"
 using closed_segment_subset by blast
 
 lemma subset_open_segment:
   fixes a :: "'a::euclidean_space"
   shows "open_segment a b \<subseteq> open_segment c d \<longleftrightarrow>
          a = b \<or> a \<in> closed_segment c d \<and> b \<in> closed_segment c d"
         (is "?lhs = ?rhs")
 proof (cases "a = b")
   case True then show ?thesis by simp
 next
   case False show ?thesis
   proof
     assume rhs: ?rhs
     with \<open>a \<noteq> b\<close> have "c \<noteq> d"
       using closed_segment_idem singleton_iff by auto
     have "\<exists>uc. (1 - u) *\<^sub>R ((1 - ua) *\<^sub>R c + ua *\<^sub>R d) + u *\<^sub>R ((1 - ub) *\<^sub>R c + ub *\<^sub>R d) =
                (1 - uc) *\<^sub>R c + uc *\<^sub>R d \<and> 0 < uc \<and> uc < 1"
         if neq: "(1 - ua) *\<^sub>R c + ua *\<^sub>R d \<noteq> (1 - ub) *\<^sub>R c + ub *\<^sub>R d" "c \<noteq> d"
            and "a = (1 - ua) *\<^sub>R c + ua *\<^sub>R d" "b = (1 - ub) *\<^sub>R c + ub *\<^sub>R d"
            and u: "0 < u" "u < 1" and uab: "0 \<le> ua" "ua \<le> 1" "0 \<le> ub" "ub \<le> 1"
         for u ua ub
     proof -
       have "ua \<noteq> ub"
         using neq by auto
       moreover have "(u - 1) * ua \<le> 0" using u uab
         by (simp add: mult_nonpos_nonneg)
       ultimately have lt: "(u - 1) * ua < u * ub" using u uab
         by (metis antisym_conv diff_ge_0_iff_ge le_less_trans mult_eq_0_iff mult_le_0_iff not_less)
       have "p * ua + q * ub < p+q" if p: "0 < p" and  q: "0 < q" for p q
       proof -
         have "\<not> p \<le> 0" "\<not> q \<le> 0"
           using p q not_less by blast+
         then show ?thesis
           by (metis \<open>ua \<noteq> ub\<close> add_less_cancel_left add_less_cancel_right add_mono_thms_linordered_field(5)
                     less_eq_real_def mult_cancel_left1 mult_less_cancel_left2 uab(2) uab(4))
       qed
       then have "(1 - u) * ua + u * ub < 1" using u \<open>ua \<noteq> ub\<close>
         by (metis diff_add_cancel diff_gt_0_iff_gt)
       with lt show ?thesis
         by (rule_tac x="ua + u*(ub-ua)" in exI) (simp add: algebra_simps)
     qed
     with rhs \<open>a \<noteq> b\<close> \<open>c \<noteq> d\<close> show ?lhs
       unfolding open_segment_image_interval closed_segment_def
       by (fastforce simp add:)
   next
     assume lhs: ?lhs
     with \<open>a \<noteq> b\<close> have "c \<noteq> d"
       by (meson finite_open_segment rev_finite_subset)
     have "closure (open_segment a b) \<subseteq> closure (open_segment c d)"
       using lhs closure_mono by blast
     then have "closed_segment a b \<subseteq> closed_segment c d"
       by (simp add: \<open>a \<noteq> b\<close> \<open>c \<noteq> d\<close>)
     then show ?rhs
       by (force simp: \<open>a \<noteq> b\<close>)
   qed
 qed
 
 lemma subset_oc_segment:
   fixes a :: "'a::euclidean_space"
   shows "open_segment a b \<subseteq> closed_segment c d \<longleftrightarrow>
          a = b \<or> a \<in> closed_segment c d \<and> b \<in> closed_segment c d"
 apply (simp add: subset_open_segment [symmetric])
 apply (rule iffI)
  apply (metis closure_closed_segment closure_mono closure_open_segment subset_closed_segment subset_open_segment)
 apply (meson dual_order.trans segment_open_subset_closed)
 done
 
 lemmas subset_segment = subset_closed_segment subset_co_segment subset_oc_segment subset_open_segment
 
 lemma dist_half_times2:
   fixes a :: "'a :: real_normed_vector"
   shows "dist ((1 / 2) *\<^sub>R (a + b)) x * 2 = dist (a+b) (2 *\<^sub>R x)"
 proof -
   have "norm ((1 / 2) *\<^sub>R (a + b) - x) * 2 = norm (2 *\<^sub>R ((1 / 2) *\<^sub>R (a + b) - x))"
     by simp
   also have "... = norm ((a + b) - 2 *\<^sub>R x)"
     by (simp add: real_vector.scale_right_diff_distrib)
   finally show ?thesis
     by (simp only: dist_norm)
 qed
 
 lemma closed_segment_as_ball:
     "closed_segment a b = affine hull {a,b} \<inter> cball(inverse 2 *\<^sub>R (a + b))(norm(b - a) / 2)"
 proof (cases "b = a")
   case True then show ?thesis by (auto simp: hull_inc)
 next
   case False
   then have *: "((\<exists>u v. x = u *\<^sub>R a + v *\<^sub>R b \<and> u + v = 1) \<and>
                   dist ((1 / 2) *\<^sub>R (a + b)) x * 2 \<le> norm (b - a)) =
                  (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> 0 \<le> u \<and> u \<le> 1)" for x
   proof -
     have "((\<exists>u v. x = u *\<^sub>R a + v *\<^sub>R b \<and> u + v = 1) \<and>
                   dist ((1 / 2) *\<^sub>R (a + b)) x * 2 \<le> norm (b - a)) =
           ((\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b) \<and>
                   dist ((1 / 2) *\<^sub>R (a + b)) x * 2 \<le> norm (b - a))"
       unfolding eq_diff_eq [symmetric] by simp
     also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
                           norm ((a+b) - (2 *\<^sub>R x)) \<le> norm (b - a))"
       by (simp add: dist_half_times2) (simp add: dist_norm)
     also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
             norm ((a+b) - (2 *\<^sub>R ((1 - u) *\<^sub>R a + u *\<^sub>R b))) \<le> norm (b - a))"
       by auto
     also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
                 norm ((1 - u * 2) *\<^sub>R (b - a)) \<le> norm (b - a))"
       by (simp add: algebra_simps scaleR_2)
     also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
                           \<bar>1 - u * 2\<bar> * norm (b - a) \<le> norm (b - a))"
       by simp
     also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> \<bar>1 - u * 2\<bar> \<le> 1)"
       by (simp add: mult_le_cancel_right2 False)
     also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> 0 \<le> u \<and> u \<le> 1)"
       by auto
     finally show ?thesis .
   qed
   show ?thesis
     by (simp add: affine_hull_2 Set.set_eq_iff closed_segment_def *)
 qed
 
 lemma open_segment_as_ball:
     "open_segment a b =
      affine hull {a,b} \<inter> ball(inverse 2 *\<^sub>R (a + b))(norm(b - a) / 2)"
 proof (cases "b = a")
   case True then show ?thesis by (auto simp: hull_inc)
 next
   case False
   then have *: "((\<exists>u v. x = u *\<^sub>R a + v *\<^sub>R b \<and> u + v = 1) \<and>
                   dist ((1 / 2) *\<^sub>R (a + b)) x * 2 < norm (b - a)) =
                  (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> 0 < u \<and> u < 1)" for x
   proof -
     have "((\<exists>u v. x = u *\<^sub>R a + v *\<^sub>R b \<and> u + v = 1) \<and>
                   dist ((1 / 2) *\<^sub>R (a + b)) x * 2 < norm (b - a)) =
           ((\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b) \<and>
                   dist ((1 / 2) *\<^sub>R (a + b)) x * 2 < norm (b - a))"
       unfolding eq_diff_eq [symmetric] by simp
     also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
                           norm ((a+b) - (2 *\<^sub>R x)) < norm (b - a))"
       by (simp add: dist_half_times2) (simp add: dist_norm)
     also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
             norm ((a+b) - (2 *\<^sub>R ((1 - u) *\<^sub>R a + u *\<^sub>R b))) < norm (b - a))"
       by auto
     also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
                 norm ((1 - u * 2) *\<^sub>R (b - a)) < norm (b - a))"
       by (simp add: algebra_simps scaleR_2)
     also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
                           \<bar>1 - u * 2\<bar> * norm (b - a) < norm (b - a))"
       by simp
     also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> \<bar>1 - u * 2\<bar> < 1)"
       by (simp add: mult_le_cancel_right2 False)
     also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> 0 < u \<and> u < 1)"
       by auto
     finally show ?thesis .
   qed
   show ?thesis
     using False by (force simp: affine_hull_2 Set.set_eq_iff open_segment_image_interval *)
 qed
 
 lemmas segment_as_ball = closed_segment_as_ball open_segment_as_ball
 
 lemma connected_segment [iff]:
   fixes x :: "'a :: real_normed_vector"
   shows "connected (closed_segment x y)"
   by (simp add: convex_connected)
 
 lemma is_interval_closed_segment_1[intro, simp]: "is_interval (closed_segment a b)" for a b::real
   unfolding closed_segment_eq_real_ivl
   by (auto simp: is_interval_def)
 
 lemma IVT'_closed_segment_real:
   fixes f :: "real \<Rightarrow> real"
   assumes "y \<in> closed_segment (f a) (f b)"
   assumes "continuous_on (closed_segment a b) f"
   shows "\<exists>x \<in> closed_segment a b. f x = y"
   using IVT'[of f a y b]
     IVT'[of "-f" a "-y" b]
     IVT'[of f b y a]
     IVT'[of "-f" b "-y" a] assms
   by (cases "a \<le> b"; cases "f b \<ge> f a") (auto simp: closed_segment_eq_real_ivl continuous_on_minus)
 
 subsection \<open>Betweenness\<close>
 
 definition\<^marker>\<open>tag important\<close> "between = (\<lambda>(a,b) x. x \<in> closed_segment a b)"
 
 lemma betweenI:
   assumes "0 \<le> u" "u \<le> 1" "x = (1 - u) *\<^sub>R a + u *\<^sub>R b"
   shows "between (a, b) x"
 using assms unfolding between_def closed_segment_def by auto
 
 lemma betweenE:
   assumes "between (a, b) x"
   obtains u where "0 \<le> u" "u \<le> 1" "x = (1 - u) *\<^sub>R a + u *\<^sub>R b"
 using assms unfolding between_def closed_segment_def by auto
 
 lemma between_implies_scaled_diff:
   assumes "between (S, T) X" "between (S, T) Y" "S \<noteq> Y"
   obtains c where "(X - Y) = c *\<^sub>R (S - Y)"
 proof -
   from \<open>between (S, T) X\<close> obtain u\<^sub>X where X: "X = u\<^sub>X *\<^sub>R S + (1 - u\<^sub>X) *\<^sub>R T"
     by (metis add.commute betweenE eq_diff_eq)
   from \<open>between (S, T) Y\<close> obtain u\<^sub>Y where Y: "Y = u\<^sub>Y *\<^sub>R S + (1 - u\<^sub>Y) *\<^sub>R T"
     by (metis add.commute betweenE eq_diff_eq)
   have "X - Y = (u\<^sub>X - u\<^sub>Y) *\<^sub>R (S - T)"
   proof -
     from X Y have "X - Y =  u\<^sub>X *\<^sub>R S - u\<^sub>Y *\<^sub>R S + ((1 - u\<^sub>X) *\<^sub>R T - (1 - u\<^sub>Y) *\<^sub>R T)" by simp
     also have "\<dots> = (u\<^sub>X - u\<^sub>Y) *\<^sub>R S - (u\<^sub>X - u\<^sub>Y) *\<^sub>R T" by (simp add: scaleR_left.diff)
     finally show ?thesis by (simp add: real_vector.scale_right_diff_distrib)
   qed
   moreover from Y have "S - Y = (1 - u\<^sub>Y) *\<^sub>R (S - T)"
     by (simp add: real_vector.scale_left_diff_distrib real_vector.scale_right_diff_distrib)
   moreover note \<open>S \<noteq> Y\<close>
   ultimately have "(X - Y) = ((u\<^sub>X - u\<^sub>Y) / (1 - u\<^sub>Y)) *\<^sub>R (S - Y)" by auto
   from this that show thesis by blast
 qed
 
 lemma between_mem_segment: "between (a,b) x \<longleftrightarrow> x \<in> closed_segment a b"
   unfolding between_def by auto
 
 lemma between: "between (a, b) (x::'a::euclidean_space) \<longleftrightarrow> dist a b = (dist a x) + (dist x b)"
 proof (cases "a = b")
   case True
   then show ?thesis
     by (auto simp add: between_def dist_commute)
 next
   case False
   then have Fal: "norm (a - b) \<noteq> 0" and Fal2: "norm (a - b) > 0"
     by auto
   have *: "\<And>u. a - ((1 - u) *\<^sub>R a + u *\<^sub>R b) = u *\<^sub>R (a - b)"
     by (auto simp add: algebra_simps)
   have "norm (a - x) *\<^sub>R (x - b) = norm (x - b) *\<^sub>R (a - x)" if "x = (1 - u) *\<^sub>R a + u *\<^sub>R b" "0 \<le> u" "u \<le> 1" for u
   proof -
     have *: "a - x = u *\<^sub>R (a - b)" "x - b = (1 - u) *\<^sub>R (a - b)"
       unfolding that(1) by (auto simp add:algebra_simps)
     show "norm (a - x) *\<^sub>R (x - b) = norm (x - b) *\<^sub>R (a - x)"
       unfolding norm_minus_commute[of x a] * using \<open>0 \<le> u\<close> \<open>u \<le> 1\<close>
       by simp
   qed
   moreover have "\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> 0 \<le> u \<and> u \<le> 1" if "dist a b = dist a x + dist x b" 
   proof -
     let ?\<beta> = "norm (a - x) / norm (a - b)"
     show "\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> 0 \<le> u \<and> u \<le> 1"
     proof (intro exI conjI)
       show "?\<beta> \<le> 1"
         using Fal2 unfolding that[unfolded dist_norm] norm_ge_zero by auto
       show "x = (1 - ?\<beta>) *\<^sub>R a + (?\<beta>) *\<^sub>R b"
       proof (subst euclidean_eq_iff; intro ballI)
         fix i :: 'a
         assume i: "i \<in> Basis"
         have "((1 - ?\<beta>) *\<^sub>R a + (?\<beta>) *\<^sub>R b) \<bullet> i 
               = ((norm (a - b) - norm (a - x)) * (a \<bullet> i) + norm (a - x) * (b \<bullet> i)) / norm (a - b)"
           using Fal by (auto simp add: field_simps inner_simps)
         also have "\<dots> = x\<bullet>i"
           apply (rule divide_eq_imp[OF Fal])
           unfolding that[unfolded dist_norm]
           using that[unfolded dist_triangle_eq] i
           apply (subst (asm) euclidean_eq_iff)
            apply (auto simp add: field_simps inner_simps)
           done
         finally show "x \<bullet> i = ((1 - ?\<beta>) *\<^sub>R a + (?\<beta>) *\<^sub>R b) \<bullet> i"
           by auto
       qed
     qed (use Fal2 in auto)
   qed
   ultimately show ?thesis
     by (force simp add: between_def closed_segment_def dist_triangle_eq)
 qed
 
 lemma between_midpoint:
   fixes a :: "'a::euclidean_space"
   shows "between (a,b) (midpoint a b)" (is ?t1)
     and "between (b,a) (midpoint a b)" (is ?t2)
 proof -
   have *: "\<And>x y z. x = (1/2::real) *\<^sub>R z \<Longrightarrow> y = (1/2) *\<^sub>R z \<Longrightarrow> norm z = norm x + norm y"
     by auto
   show ?t1 ?t2
     unfolding between midpoint_def dist_norm
     by (auto simp add: field_simps inner_simps euclidean_eq_iff[where 'a='a] intro!: *)
 qed
 
 lemma between_mem_convex_hull:
   "between (a,b) x \<longleftrightarrow> x \<in> convex hull {a,b}"
   unfolding between_mem_segment segment_convex_hull ..
 
 lemma between_triv_iff [simp]: "between (a,a) b \<longleftrightarrow> a=b"
   by (auto simp: between_def)
 
 lemma between_triv1 [simp]: "between (a,b) a"
   by (auto simp: between_def)
 
 lemma between_triv2 [simp]: "between (a,b) b"
   by (auto simp: between_def)
 
 lemma between_commute:
    "between (a,b) = between (b,a)"
 by (auto simp: between_def closed_segment_commute)
 
 lemma between_antisym:
   fixes a :: "'a :: euclidean_space"
   shows "\<lbrakk>between (b,c) a; between (a,c) b\<rbrakk> \<Longrightarrow> a = b"
 by (auto simp: between dist_commute)
 
 lemma between_trans:
     fixes a :: "'a :: euclidean_space"
     shows "\<lbrakk>between (b,c) a; between (a,c) d\<rbrakk> \<Longrightarrow> between (b,c) d"
   using dist_triangle2 [of b c d] dist_triangle3 [of b d a]
   by (auto simp: between dist_commute)
 
 lemma between_norm:
     fixes a :: "'a :: euclidean_space"
     shows "between (a,b) x \<longleftrightarrow> norm(x - a) *\<^sub>R (b - x) = norm(b - x) *\<^sub>R (x - a)"
   by (auto simp: between dist_triangle_eq norm_minus_commute algebra_simps)
 
 lemma between_swap:
   fixes A B X Y :: "'a::euclidean_space"
   assumes "between (A, B) X"
   assumes "between (A, B) Y"
   shows "between (X, B) Y \<longleftrightarrow> between (A, Y) X"
 using assms by (auto simp add: between)
 
 lemma between_translation [simp]: "between (a + y,a + z) (a + x) \<longleftrightarrow> between (y,z) x"
   by (auto simp: between_def)
 
 lemma between_trans_2:
   fixes a :: "'a :: euclidean_space"
   shows "\<lbrakk>between (b,c) a; between (a,b) d\<rbrakk> \<Longrightarrow> between (c,d) a"
   by (metis between_commute between_swap between_trans)
 
 lemma between_scaleR_lift [simp]:
   fixes v :: "'a::euclidean_space"
   shows "between (a *\<^sub>R v, b *\<^sub>R v) (c *\<^sub>R v) \<longleftrightarrow> v = 0 \<or> between (a, b) c"
   by (simp add: between dist_norm scaleR_left_diff_distrib [symmetric] distrib_right [symmetric])
 
 lemma between_1:
   fixes x::real
   shows "between (a,b) x \<longleftrightarrow> (a \<le> x \<and> x \<le> b) \<or> (b \<le> x \<and> x \<le> a)"
   by (auto simp: between_mem_segment closed_segment_eq_real_ivl)
 
 end
\ No newline at end of file
diff --git a/src/HOL/Analysis/Topology_Euclidean_Space.thy b/src/HOL/Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy
@@ -1,2508 +1,2579 @@
 (*  Author:     L C Paulson, University of Cambridge
     Author:     Amine Chaieb, University of Cambridge
     Author:     Robert Himmelmann, TU Muenchen
     Author:     Brian Huffman, Portland State University
 *)
 
 chapter \<open>Vector Analysis\<close>
 
 theory Topology_Euclidean_Space
   imports
     Elementary_Normed_Spaces
     Linear_Algebra
     Norm_Arith
 begin
 
 section \<open>Elementary Topology in Euclidean Space\<close>
 
 lemma euclidean_dist_l2:
   fixes x y :: "'a :: euclidean_space"
   shows "dist x y = L2_set (\<lambda>i. dist (x \<bullet> i) (y \<bullet> i)) Basis"
   unfolding dist_norm norm_eq_sqrt_inner L2_set_def
   by (subst euclidean_inner) (simp add: power2_eq_square inner_diff_left)
 
 lemma norm_nth_le: "norm (x \<bullet> i) \<le> norm x" if "i \<in> Basis"
 proof -
   have "(x \<bullet> i)\<^sup>2 = (\<Sum>i\<in>{i}. (x \<bullet> i)\<^sup>2)"
     by simp
   also have "\<dots> \<le> (\<Sum>i\<in>Basis. (x \<bullet> i)\<^sup>2)"
     by (intro sum_mono2) (auto simp: that)
   finally show ?thesis
     unfolding norm_conv_dist euclidean_dist_l2[of x] L2_set_def
     by (auto intro!: real_le_rsqrt)
 qed
 
 subsection\<^marker>\<open>tag unimportant\<close> \<open>Continuity of the representation WRT an orthogonal basis\<close>
 
 lemma orthogonal_Basis: "pairwise orthogonal Basis"
   by (simp add: inner_not_same_Basis orthogonal_def pairwise_def)
 
 lemma representation_bound:
   fixes B :: "'N::real_inner set"
   assumes "finite B" "independent B" "b \<in> B" and orth: "pairwise orthogonal B"
   obtains m where "m > 0" "\<And>x. x \<in> span B \<Longrightarrow> \<bar>representation B x b\<bar> \<le> m * norm x"
 proof 
   fix x
   assume x: "x \<in> span B"
   have "b \<noteq> 0"
     using \<open>independent B\<close> \<open>b \<in> B\<close> dependent_zero by blast
   have [simp]: "b \<bullet> b' = (if b' = b then (norm b)\<^sup>2 else 0)"
     if "b \<in> B" "b' \<in> B" for b b'
     using orth by (simp add: orthogonal_def pairwise_def norm_eq_sqrt_inner that)
   have "norm x = norm (\<Sum>b\<in>B. representation B x b *\<^sub>R b)"
     using real_vector.sum_representation_eq [OF \<open>independent B\<close> x \<open>finite B\<close> order_refl]
     by simp
   also have "\<dots> = sqrt ((\<Sum>b\<in>B. representation B x b *\<^sub>R b) \<bullet> (\<Sum>b\<in>B. representation B x b *\<^sub>R b))"
     by (simp add: norm_eq_sqrt_inner)
   also have "\<dots> = sqrt (\<Sum>b\<in>B. (representation B x b *\<^sub>R b) \<bullet> (representation B x b *\<^sub>R b))"
     using \<open>finite B\<close>
     by (simp add: inner_sum_left inner_sum_right if_distrib [of "\<lambda>x. _ * x"] cong: if_cong sum.cong_simp)
   also have "\<dots> = sqrt (\<Sum>b\<in>B. (norm (representation B x b *\<^sub>R b))\<^sup>2)"
     by (simp add: mult.commute mult.left_commute power2_eq_square)
   also have "\<dots> = sqrt (\<Sum>b\<in>B. (representation B x b)\<^sup>2 * (norm b)\<^sup>2)"
     by (simp add: norm_mult power_mult_distrib)
   finally have "norm x = sqrt (\<Sum>b\<in>B. (representation B x b)\<^sup>2 * (norm b)\<^sup>2)" .
   moreover
   have "sqrt ((representation B x b)\<^sup>2 * (norm b)\<^sup>2) \<le> sqrt (\<Sum>b\<in>B. (representation B x b)\<^sup>2 * (norm b)\<^sup>2)"
     using \<open>b \<in> B\<close> \<open>finite B\<close> by (auto intro: member_le_sum)
   then have "\<bar>representation B x b\<bar> \<le> (1 / norm b) * sqrt (\<Sum>b\<in>B. (representation B x b)\<^sup>2 * (norm b)\<^sup>2)"
     using \<open>b \<noteq> 0\<close> by (simp add: field_split_simps real_sqrt_mult del: real_sqrt_le_iff)
   ultimately show "\<bar>representation B x b\<bar> \<le> (1 / norm b) * norm x"
     by simp
 next
   show "0 < 1 / norm b"
     using \<open>independent B\<close> \<open>b \<in> B\<close> dependent_zero by auto
 qed 
 
 lemma continuous_on_representation:
   fixes B :: "'N::euclidean_space set"
   assumes "finite B" "independent B" "b \<in> B" "pairwise orthogonal B" 
   shows "continuous_on (span B) (\<lambda>x. representation B x b)"
 proof
   show "\<exists>d>0. \<forall>x'\<in>span B. dist x' x < d \<longrightarrow> dist (representation B x' b) (representation B x b) \<le> e"
     if "e > 0" "x \<in> span B" for x e
   proof -
     obtain m where "m > 0" and m: "\<And>x. x \<in> span B \<Longrightarrow> \<bar>representation B x b\<bar> \<le> m * norm x"
       using assms representation_bound by blast
     show ?thesis
       unfolding dist_norm
     proof (intro exI conjI ballI impI)
       show "e/m > 0"
         by (simp add: \<open>e > 0\<close> \<open>m > 0\<close>)
       show "norm (representation B x' b - representation B x b) \<le> e"
         if x': "x' \<in> span B" and less: "norm (x'-x) < e/m" for x' 
       proof -
         have "\<bar>representation B (x'-x) b\<bar> \<le> m * norm (x'-x)"
           using m [of "x'-x"] \<open>x \<in> span B\<close> span_diff x' by blast
         also have "\<dots> < e"
           by (metis \<open>m > 0\<close> less mult.commute pos_less_divide_eq)
         finally have "\<bar>representation B (x'-x) b\<bar> \<le> e" by simp
         then show ?thesis
           by (simp add: \<open>x \<in> span B\<close> \<open>independent B\<close> representation_diff x')
       qed
     qed
   qed
 qed
 
 subsection\<^marker>\<open>tag unimportant\<close>\<open>Balls in Euclidean Space\<close>
 
 lemma cball_subset_cball_iff:
   fixes a :: "'a :: euclidean_space"
   shows "cball a r \<subseteq> cball a' r' \<longleftrightarrow> dist a a' + r \<le> r' \<or> r < 0"
     (is "?lhs \<longleftrightarrow> ?rhs")
 proof
   assume ?lhs
   then show ?rhs
   proof (cases "r < 0")
     case True
     then show ?rhs by simp
   next
     case False
     then have [simp]: "r \<ge> 0" by simp
     have "norm (a - a') + r \<le> r'"
     proof (cases "a = a'")
       case True
       then show ?thesis
         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>]
         by (force simp: SOME_Basis dist_norm)
     next
       case False
       have "norm (a' - (a + (r / norm (a - a')) *\<^sub>R (a - a'))) = norm (a' - a - (r / norm (a - a')) *\<^sub>R (a - a'))"
         by (simp add: algebra_simps)
       also have "... = norm ((-1 - (r / norm (a - a'))) *\<^sub>R (a - a'))"
         by (simp add: algebra_simps)
       also from \<open>a \<noteq> a'\<close> have "... = \<bar>- norm (a - a') - r\<bar>"
         by simp (simp add: field_simps)
       finally have [simp]: "norm (a' - (a + (r / norm (a - a')) *\<^sub>R (a - a'))) = \<bar>norm (a - a') + r\<bar>"
         by linarith
       from \<open>a \<noteq> a'\<close> show ?thesis
         using subsetD [where c = "a' + (1 + r / norm(a - a')) *\<^sub>R (a - a')", OF \<open>?lhs\<close>]
         by (simp add: dist_norm scaleR_add_left)
     qed
     then show ?rhs
       by (simp add: dist_norm)
   qed
 qed metric
 
 lemma cball_subset_ball_iff: "cball a r \<subseteq> ball a' r' \<longleftrightarrow> dist a a' + r < r' \<or> r < 0"
   (is "?lhs \<longleftrightarrow> ?rhs")
   for a :: "'a::euclidean_space"
 proof
   assume ?lhs
   then show ?rhs
   proof (cases "r < 0")
     case True then
     show ?rhs by simp
   next
     case False
     then have [simp]: "r \<ge> 0" by simp
     have "norm (a - a') + r < r'"
     proof (cases "a = a'")
       case True
       then show ?thesis
         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>]
         by (force simp: SOME_Basis dist_norm)
     next
       case False
       have False if "norm (a - a') + r \<ge> r'"
       proof -
         from that have "\<bar>r' - norm (a - a')\<bar> \<le> r"
           by (simp split: abs_split)
             (metis \<open>0 \<le> r\<close> \<open>?lhs\<close> centre_in_cball dist_commute dist_norm less_asym mem_ball subset_eq)
         then show ?thesis
           using subsetD [where c = "a + (r' / norm(a - a') - 1) *\<^sub>R (a - a')", OF \<open>?lhs\<close>] \<open>a \<noteq> a'\<close>
           apply (simp add: dist_norm)
           apply (simp add: scaleR_left_diff_distrib)
           apply (simp add: field_simps)
           done
       qed
       then show ?thesis by force
     qed
     then show ?rhs by (simp add: dist_norm)
   qed
 next
   assume ?rhs
   then show ?lhs
     by metric
 qed
 
 lemma ball_subset_cball_iff: "ball a r \<subseteq> cball a' r' \<longleftrightarrow> dist a a' + r \<le> r' \<or> r \<le> 0"
   (is "?lhs = ?rhs")
   for a :: "'a::euclidean_space"
 proof (cases "r \<le> 0")
   case True
   then show ?thesis
     by metric
 next
   case False
   show ?thesis
   proof
     assume ?lhs
     then have "(cball a r \<subseteq> cball a' r')"
       by (metis False closed_cball closure_ball closure_closed closure_mono not_less)
     with False show ?rhs
       by (fastforce iff: cball_subset_cball_iff)
   next
     assume ?rhs
     with False show ?lhs
       by metric
   qed
 qed
 
 lemma ball_subset_ball_iff:
   fixes a :: "'a :: euclidean_space"
   shows "ball a r \<subseteq> ball a' r' \<longleftrightarrow> dist a a' + r \<le> r' \<or> r \<le> 0"
         (is "?lhs = ?rhs")
 proof (cases "r \<le> 0")
   case True then show ?thesis
     by metric
 next
   case False show ?thesis
   proof
     assume ?lhs
     then have "0 < r'"
       using False by metric
     then have "(cball a r \<subseteq> cball a' r')"
       by (metis False\<open>?lhs\<close> closure_ball closure_mono not_less)
     then show ?rhs
       using False cball_subset_cball_iff by fastforce
   qed metric
 qed
 
 
 lemma ball_eq_ball_iff:
   fixes x :: "'a :: euclidean_space"
   shows "ball x d = ball y e \<longleftrightarrow> d \<le> 0 \<and> e \<le> 0 \<or> x=y \<and> d=e"
         (is "?lhs = ?rhs")
 proof
   assume ?lhs
   then show ?rhs
   proof (cases "d \<le> 0 \<or> e \<le> 0")
     case True
       with \<open>?lhs\<close> show ?rhs
         by safe (simp_all only: ball_eq_empty [of y e, symmetric] ball_eq_empty [of x d, symmetric])
   next
     case False
     with \<open>?lhs\<close> show ?rhs
       apply (auto simp: set_eq_subset ball_subset_ball_iff dist_norm norm_minus_commute algebra_simps)
       apply (metis add_le_same_cancel1 le_add_same_cancel1 norm_ge_zero norm_pths(2) order_trans)
       apply (metis add_increasing2 add_le_imp_le_right eq_iff norm_ge_zero)
       done
   qed
 next
   assume ?rhs then show ?lhs
     by (auto simp: set_eq_subset ball_subset_ball_iff)
 qed
 
 lemma cball_eq_cball_iff:
   fixes x :: "'a :: euclidean_space"
   shows "cball x d = cball y e \<longleftrightarrow> d < 0 \<and> e < 0 \<or> x=y \<and> d=e"
         (is "?lhs = ?rhs")
 proof
   assume ?lhs
   then show ?rhs
   proof (cases "d < 0 \<or> e < 0")
     case True
       with \<open>?lhs\<close> show ?rhs
         by safe (simp_all only: cball_eq_empty [of y e, symmetric] cball_eq_empty [of x d, symmetric])
   next
     case False
     with \<open>?lhs\<close> show ?rhs
       apply (auto simp: set_eq_subset cball_subset_cball_iff dist_norm norm_minus_commute algebra_simps)
       apply (metis add_le_same_cancel1 le_add_same_cancel1 norm_ge_zero norm_pths(2) order_trans)
       apply (metis add_increasing2 add_le_imp_le_right eq_iff norm_ge_zero)
       done
   qed
 next
   assume ?rhs then show ?lhs
     by (auto simp: set_eq_subset cball_subset_cball_iff)
 qed
 
 lemma ball_eq_cball_iff:
   fixes x :: "'a :: euclidean_space"
   shows "ball x d = cball y e \<longleftrightarrow> d \<le> 0 \<and> e < 0" (is "?lhs = ?rhs")
 proof
   assume ?lhs
   then show ?rhs
     apply (auto simp: set_eq_subset ball_subset_cball_iff cball_subset_ball_iff algebra_simps)
     apply (metis add_increasing2 add_le_cancel_right add_less_same_cancel1 dist_not_less_zero less_le_trans zero_le_dist)
     apply (metis add_less_same_cancel1 dist_not_less_zero less_le_trans not_le)
     using \<open>?lhs\<close> ball_eq_empty cball_eq_empty apply blast+
     done
 next
   assume ?rhs then show ?lhs by auto
 qed
 
 lemma cball_eq_ball_iff:
   fixes x :: "'a :: euclidean_space"
   shows "cball x d = ball y e \<longleftrightarrow> d < 0 \<and> e \<le> 0"
   using ball_eq_cball_iff by blast
 
 lemma finite_ball_avoid:
   fixes S :: "'a :: euclidean_space set"
   assumes "open S" "finite X" "p \<in> S"
   shows "\<exists>e>0. \<forall>w\<in>ball p e. w\<in>S \<and> (w\<noteq>p \<longrightarrow> w\<notin>X)"
 proof -
   obtain e1 where "0 < e1" and e1_b:"ball p e1 \<subseteq> S"
     using open_contains_ball_eq[OF \<open>open S\<close>] assms by auto
   obtain e2 where "0 < e2" and "\<forall>x\<in>X. x \<noteq> p \<longrightarrow> e2 \<le> dist p x"
     using finite_set_avoid[OF \<open>finite X\<close>,of p] by auto
   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
   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>
     apply (rule_tac x="min e1 e2" in exI)
     by auto
 qed
 
 lemma finite_cball_avoid:
   fixes S :: "'a :: euclidean_space set"
   assumes "open S" "finite X" "p \<in> S"
   shows "\<exists>e>0. \<forall>w\<in>cball p e. w\<in>S \<and> (w\<noteq>p \<longrightarrow> w\<notin>X)"
 proof -
   obtain e1 where "e1>0" and e1: "\<forall>w\<in>ball p e1. w\<in>S \<and> (w\<noteq>p \<longrightarrow> w\<notin>X)"
     using finite_ball_avoid[OF assms] by auto
   define e2 where "e2 \<equiv> e1/2"
   have "e2>0" and "e2 < e1" unfolding e2_def using \<open>e1>0\<close> by auto
   then have "cball p e2 \<subseteq> ball p e1" by (subst cball_subset_ball_iff,auto)
   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
 qed
 
 lemma dim_cball:
   assumes "e > 0"
   shows "dim (cball (0 :: 'n::euclidean_space) e) = DIM('n)"
 proof -
   {
     fix x :: "'n::euclidean_space"
     define y where "y = (e / norm x) *\<^sub>R x"
     then have "y \<in> cball 0 e"
       using assms by auto
     moreover have *: "x = (norm x / e) *\<^sub>R y"
       using y_def assms by simp
     moreover from * have "x = (norm x/e) *\<^sub>R y"
       by auto
     ultimately have "x \<in> span (cball 0 e)"
       using span_scale[of y "cball 0 e" "norm x/e"]
         span_superset[of "cball 0 e"]
       by (simp add: span_base)
   }
   then have "span (cball 0 e) = (UNIV :: 'n::euclidean_space set)"
     by auto
   then show ?thesis
     using dim_span[of "cball (0 :: 'n::euclidean_space) e"] by (auto)
 qed
 
 
 subsection \<open>Boxes\<close>
 
 abbreviation\<^marker>\<open>tag important\<close> One :: "'a::euclidean_space" where
 "One \<equiv> \<Sum>Basis"
 
 lemma One_non_0: assumes "One = (0::'a::euclidean_space)" shows False
 proof -
   have "dependent (Basis :: 'a set)"
     apply (simp add: dependent_finite)
     apply (rule_tac x="\<lambda>i. 1" in exI)
     using SOME_Basis apply (auto simp: assms)
     done
   with independent_Basis show False by force
 qed
 
 corollary\<^marker>\<open>tag unimportant\<close> One_neq_0[iff]: "One \<noteq> 0"
   by (metis One_non_0)
 
 corollary\<^marker>\<open>tag unimportant\<close> Zero_neq_One[iff]: "0 \<noteq> One"
   by (metis One_non_0)
 
 definition\<^marker>\<open>tag important\<close> (in euclidean_space) eucl_less (infix "<e" 50) where 
 "eucl_less a b \<longleftrightarrow> (\<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i)"
 
 definition\<^marker>\<open>tag important\<close> box_eucl_less: "box a b = {x. a <e x \<and> x <e b}"
 definition\<^marker>\<open>tag important\<close> "cbox a b = {x. \<forall>i\<in>Basis. a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i}"
 
 lemma box_def: "box a b = {x. \<forall>i\<in>Basis. a \<bullet> i < x \<bullet> i \<and> x \<bullet> i < b \<bullet> i}"
   and in_box_eucl_less: "x \<in> box a b \<longleftrightarrow> a <e x \<and> x <e b"
   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)"
     "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)"
   by (auto simp: box_eucl_less eucl_less_def cbox_def)
 
 lemma cbox_Pair_eq: "cbox (a, c) (b, d) = cbox a b \<times> cbox c d"
   by (force simp: cbox_def Basis_prod_def)
 
 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"
   by (force simp: cbox_Pair_eq)
 
 lemma cbox_Complex_eq: "cbox (Complex a c) (Complex b d) = (\<lambda>(x,y). Complex x y) ` (cbox a b \<times> cbox c d)"
   apply (auto simp: cbox_def Basis_complex_def)
   apply (rule_tac x = "(Re x, Im x)" in image_eqI)
   using complex_eq by auto
 
 lemma cbox_Pair_eq_0: "cbox (a, c) (b, d) = {} \<longleftrightarrow> cbox a b = {} \<or> cbox c d = {}"
   by (force simp: cbox_Pair_eq)
 
 lemma swap_cbox_Pair [simp]: "prod.swap ` cbox (c, a) (d, b) = cbox (a,c) (b,d)"
   by auto
 
 lemma mem_box_real[simp]:
   "(x::real) \<in> box a b \<longleftrightarrow> a < x \<and> x < b"
   "(x::real) \<in> cbox a b \<longleftrightarrow> a \<le> x \<and> x \<le> b"
   by (auto simp: mem_box)
 
 lemma box_real[simp]:
   fixes a b:: real
   shows "box a b = {a <..< b}" "cbox a b = {a .. b}"
   by auto
 
 lemma box_Int_box:
   fixes a :: "'a::euclidean_space"
   shows "box a b \<inter> box c d =
     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)"
   unfolding set_eq_iff and Int_iff and mem_box by auto
 
 lemma rational_boxes:
   fixes x :: "'a::euclidean_space"
   assumes "e > 0"
   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"
 proof -
   define e' where "e' = e / (2 * sqrt (real (DIM ('a))))"
   then have e: "e' > 0"
     using assms by (auto)
   have "\<forall>i. \<exists>y. y \<in> \<rat> \<and> y < x \<bullet> i \<and> x \<bullet> i - y < e'" (is "\<forall>i. ?th i")
   proof
     fix i
     from Rats_dense_in_real[of "x \<bullet> i - e'" "x \<bullet> i"] e
     show "?th i" by auto
   qed
   from choice[OF this] obtain a where
     a: "\<forall>xa. a xa \<in> \<rat> \<and> a xa < x \<bullet> xa \<and> x \<bullet> xa - a xa < e'" ..
   have "\<forall>i. \<exists>y. y \<in> \<rat> \<and> x \<bullet> i < y \<and> y - x \<bullet> i < e'" (is "\<forall>i. ?th i")
   proof
     fix i
     from Rats_dense_in_real[of "x \<bullet> i" "x \<bullet> i + e'"] e
     show "?th i" by auto
   qed
   from choice[OF this] obtain b where
     b: "\<forall>xa. b xa \<in> \<rat> \<and> x \<bullet> xa < b xa \<and> b xa - x \<bullet> xa < e'" ..
   let ?a = "\<Sum>i\<in>Basis. a i *\<^sub>R i" and ?b = "\<Sum>i\<in>Basis. b i *\<^sub>R i"
   show ?thesis
   proof (rule exI[of _ ?a], rule exI[of _ ?b], safe)
     fix y :: 'a
     assume *: "y \<in> box ?a ?b"
     have "dist x y = sqrt (\<Sum>i\<in>Basis. (dist (x \<bullet> i) (y \<bullet> i))\<^sup>2)"
       unfolding L2_set_def[symmetric] by (rule euclidean_dist_l2)
     also have "\<dots> < sqrt (\<Sum>(i::'a)\<in>Basis. e^2 / real (DIM('a)))"
     proof (rule real_sqrt_less_mono, rule sum_strict_mono)
       fix i :: "'a"
       assume i: "i \<in> Basis"
       have "a i < y\<bullet>i \<and> y\<bullet>i < b i"
         using * i by (auto simp: box_def)
       moreover have "a i < x\<bullet>i" "x\<bullet>i - a i < e'"
         using a by auto
       moreover have "x\<bullet>i < b i" "b i - x\<bullet>i < e'"
         using b by auto
       ultimately have "\<bar>x\<bullet>i - y\<bullet>i\<bar> < 2 * e'"
         by auto
       then have "dist (x \<bullet> i) (y \<bullet> i) < e/sqrt (real (DIM('a)))"
         unfolding e'_def by (auto simp: dist_real_def)
       then have "(dist (x \<bullet> i) (y \<bullet> i))\<^sup>2 < (e/sqrt (real (DIM('a))))\<^sup>2"
         by (rule power_strict_mono) auto
       then show "(dist (x \<bullet> i) (y \<bullet> i))\<^sup>2 < e\<^sup>2 / real DIM('a)"
         by (simp add: power_divide)
     qed auto
     also have "\<dots> = e"
       using \<open>0 < e\<close> by simp
     finally show "y \<in> ball x e"
       by (auto simp: ball_def)
   qed (insert a b, auto simp: box_def)
 qed
 
 lemma open_UNION_box:
   fixes M :: "'a::euclidean_space set"
   assumes "open M"
   defines "a' \<equiv> \<lambda>f :: 'a \<Rightarrow> real \<times> real. (\<Sum>(i::'a)\<in>Basis. fst (f i) *\<^sub>R i)"
   defines "b' \<equiv> \<lambda>f :: 'a \<Rightarrow> real \<times> real. (\<Sum>(i::'a)\<in>Basis. snd (f i) *\<^sub>R i)"
   defines "I \<equiv> {f\<in>Basis \<rightarrow>\<^sub>E \<rat> \<times> \<rat>. box (a' f) (b' f) \<subseteq> M}"
   shows "M = (\<Union>f\<in>I. box (a' f) (b' f))"
 proof -
   have "x \<in> (\<Union>f\<in>I. box (a' f) (b' f))" if "x \<in> M" for x
   proof -
     obtain e where e: "e > 0" "ball x e \<subseteq> M"
       using openE[OF \<open>open M\<close> \<open>x \<in> M\<close>] by auto
     moreover obtain a b where ab:
       "x \<in> box a b"
       "\<forall>i \<in> Basis. a \<bullet> i \<in> \<rat>"
       "\<forall>i\<in>Basis. b \<bullet> i \<in> \<rat>"
       "box a b \<subseteq> ball x e"
       using rational_boxes[OF e(1)] by metis
     ultimately show ?thesis
        by (intro UN_I[of "\<lambda>i\<in>Basis. (a \<bullet> i, b \<bullet> i)"])
           (auto simp: euclidean_representation I_def a'_def b'_def)
   qed
   then show ?thesis by (auto simp: I_def)
 qed
 
 corollary open_countable_Union_open_box:
   fixes S :: "'a :: euclidean_space set"
   assumes "open S"
   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"
 proof -
   let ?a = "\<lambda>f. (\<Sum>(i::'a)\<in>Basis. fst (f i) *\<^sub>R i)"
   let ?b = "\<lambda>f. (\<Sum>(i::'a)\<in>Basis. snd (f i) *\<^sub>R i)"
   let ?I = "{f\<in>Basis \<rightarrow>\<^sub>E \<rat> \<times> \<rat>. box (?a f) (?b f) \<subseteq> S}"
   let ?\<D> = "(\<lambda>f. box (?a f) (?b f)) ` ?I"
   show ?thesis
   proof
     have "countable ?I"
       by (simp add: countable_PiE countable_rat)
     then show "countable ?\<D>"
       by blast
     show "\<Union>?\<D> = S"
       using open_UNION_box [OF assms] by metis
   qed auto
 qed
 
 lemma rational_cboxes:
   fixes x :: "'a::euclidean_space"
   assumes "e > 0"
   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"
 proof -
   define e' where "e' = e / (2 * sqrt (real (DIM ('a))))"
   then have e: "e' > 0"
     using assms by auto
   have "\<forall>i. \<exists>y. y \<in> \<rat> \<and> y < x \<bullet> i \<and> x \<bullet> i - y < e'" (is "\<forall>i. ?th i")
   proof
     fix i
     from Rats_dense_in_real[of "x \<bullet> i - e'" "x \<bullet> i"] e
     show "?th i" by auto
   qed
   from choice[OF this] obtain a where
     a: "\<forall>u. a u \<in> \<rat> \<and> a u < x \<bullet> u \<and> x \<bullet> u - a u < e'" ..
   have "\<forall>i. \<exists>y. y \<in> \<rat> \<and> x \<bullet> i < y \<and> y - x \<bullet> i < e'" (is "\<forall>i. ?th i")
   proof
     fix i
     from Rats_dense_in_real[of "x \<bullet> i" "x \<bullet> i + e'"] e
     show "?th i" by auto
   qed
   from choice[OF this] obtain b where
     b: "\<forall>u. b u \<in> \<rat> \<and> x \<bullet> u < b u \<and> b u - x \<bullet> u < e'" ..
   let ?a = "\<Sum>i\<in>Basis. a i *\<^sub>R i" and ?b = "\<Sum>i\<in>Basis. b i *\<^sub>R i"
   show ?thesis
   proof (rule exI[of _ ?a], rule exI[of _ ?b], safe)
     fix y :: 'a
     assume *: "y \<in> cbox ?a ?b"
     have "dist x y = sqrt (\<Sum>i\<in>Basis. (dist (x \<bullet> i) (y \<bullet> i))\<^sup>2)"
       unfolding L2_set_def[symmetric] by (rule euclidean_dist_l2)
     also have "\<dots> < sqrt (\<Sum>(i::'a)\<in>Basis. e^2 / real (DIM('a)))"
     proof (rule real_sqrt_less_mono, rule sum_strict_mono)
       fix i :: "'a"
       assume i: "i \<in> Basis"
       have "a i \<le> y\<bullet>i \<and> y\<bullet>i \<le> b i"
         using * i by (auto simp: cbox_def)
       moreover have "a i < x\<bullet>i" "x\<bullet>i - a i < e'"
         using a by auto
       moreover have "x\<bullet>i < b i" "b i - x\<bullet>i < e'"
         using b by auto
       ultimately have "\<bar>x\<bullet>i - y\<bullet>i\<bar> < 2 * e'"
         by auto
       then have "dist (x \<bullet> i) (y \<bullet> i) < e/sqrt (real (DIM('a)))"
         unfolding e'_def by (auto simp: dist_real_def)
       then have "(dist (x \<bullet> i) (y \<bullet> i))\<^sup>2 < (e/sqrt (real (DIM('a))))\<^sup>2"
         by (rule power_strict_mono) auto
       then show "(dist (x \<bullet> i) (y \<bullet> i))\<^sup>2 < e\<^sup>2 / real DIM('a)"
         by (simp add: power_divide)
     qed auto
     also have "\<dots> = e"
       using \<open>0 < e\<close> by simp
     finally show "y \<in> ball x e"
       by (auto simp: ball_def)
   next
     show "x \<in> cbox (\<Sum>i\<in>Basis. a i *\<^sub>R i) (\<Sum>i\<in>Basis. b i *\<^sub>R i)"
       using a b less_imp_le by (auto simp: cbox_def)
   qed (use a b cbox_def in auto)
 qed
 
 lemma open_UNION_cbox:
   fixes M :: "'a::euclidean_space set"
   assumes "open M"
   defines "a' \<equiv> \<lambda>f. (\<Sum>(i::'a)\<in>Basis. fst (f i) *\<^sub>R i)"
   defines "b' \<equiv> \<lambda>f. (\<Sum>(i::'a)\<in>Basis. snd (f i) *\<^sub>R i)"
   defines "I \<equiv> {f\<in>Basis \<rightarrow>\<^sub>E \<rat> \<times> \<rat>. cbox (a' f) (b' f) \<subseteq> M}"
   shows "M = (\<Union>f\<in>I. cbox (a' f) (b' f))"
 proof -
   have "x \<in> (\<Union>f\<in>I. cbox (a' f) (b' f))" if "x \<in> M" for x
   proof -
     obtain e where e: "e > 0" "ball x e \<subseteq> M"
       using openE[OF \<open>open M\<close> \<open>x \<in> M\<close>] by auto
     moreover obtain a b where ab: "x \<in> cbox a b" "\<forall>i \<in> Basis. a \<bullet> i \<in> \<rat>"
                                   "\<forall>i \<in> Basis. b \<bullet> i \<in> \<rat>" "cbox a b \<subseteq> ball x e"
       using rational_cboxes[OF e(1)] by metis
     ultimately show ?thesis
        by (intro UN_I[of "\<lambda>i\<in>Basis. (a \<bullet> i, b \<bullet> i)"])
           (auto simp: euclidean_representation I_def a'_def b'_def)
   qed
   then show ?thesis by (auto simp: I_def)
 qed
 
 corollary open_countable_Union_open_cbox:
   fixes S :: "'a :: euclidean_space set"
   assumes "open S"
   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"
 proof -
   let ?a = "\<lambda>f. (\<Sum>(i::'a)\<in>Basis. fst (f i) *\<^sub>R i)"
   let ?b = "\<lambda>f. (\<Sum>(i::'a)\<in>Basis. snd (f i) *\<^sub>R i)"
   let ?I = "{f\<in>Basis \<rightarrow>\<^sub>E \<rat> \<times> \<rat>. cbox (?a f) (?b f) \<subseteq> S}"
   let ?\<D> = "(\<lambda>f. cbox (?a f) (?b f)) ` ?I"
   show ?thesis
   proof
     have "countable ?I"
       by (simp add: countable_PiE countable_rat)
     then show "countable ?\<D>"
       by blast
     show "\<Union>?\<D> = S"
       using open_UNION_cbox [OF assms] by metis
   qed auto
 qed
 
 lemma box_eq_empty:
   fixes a :: "'a::euclidean_space"
   shows "(box a b = {} \<longleftrightarrow> (\<exists>i\<in>Basis. b\<bullet>i \<le> a\<bullet>i))" (is ?th1)
     and "(cbox a b = {} \<longleftrightarrow> (\<exists>i\<in>Basis. b\<bullet>i < a\<bullet>i))" (is ?th2)
 proof -
   {
     fix i x
     assume i: "i\<in>Basis" and as:"b\<bullet>i \<le> a\<bullet>i" and x:"x\<in>box a b"
     then have "a \<bullet> i < x \<bullet> i \<and> x \<bullet> i < b \<bullet> i"
       unfolding mem_box by (auto simp: box_def)
     then have "a\<bullet>i < b\<bullet>i" by auto
     then have False using as by auto
   }
   moreover
   {
     assume as: "\<forall>i\<in>Basis. \<not> (b\<bullet>i \<le> a\<bullet>i)"
     let ?x = "(1/2) *\<^sub>R (a + b)"
     {
       fix i :: 'a
       assume i: "i \<in> Basis"
       have "a\<bullet>i < b\<bullet>i"
         using as[THEN bspec[where x=i]] i by auto
       then have "a\<bullet>i < ((1/2) *\<^sub>R (a+b)) \<bullet> i" "((1/2) *\<^sub>R (a+b)) \<bullet> i < b\<bullet>i"
         by (auto simp: inner_add_left)
     }
     then have "box a b \<noteq> {}"
       using mem_box(1)[of "?x" a b] by auto
   }
   ultimately show ?th1 by blast
 
   {
     fix i x
     assume i: "i \<in> Basis" and as:"b\<bullet>i < a\<bullet>i" and x:"x\<in>cbox a b"
     then have "a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i"
       unfolding mem_box by auto
     then have "a\<bullet>i \<le> b\<bullet>i" by auto
     then have False using as by auto
   }
   moreover
   {
     assume as:"\<forall>i\<in>Basis. \<not> (b\<bullet>i < a\<bullet>i)"
     let ?x = "(1/2) *\<^sub>R (a + b)"
     {
       fix i :: 'a
       assume i:"i \<in> Basis"
       have "a\<bullet>i \<le> b\<bullet>i"
         using as[THEN bspec[where x=i]] i by auto
       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"
         by (auto simp: inner_add_left)
     }
     then have "cbox a b \<noteq> {}"
       using mem_box(2)[of "?x" a b] by auto
   }
   ultimately show ?th2 by blast
 qed
 
 lemma box_ne_empty:
   fixes a :: "'a::euclidean_space"
   shows "cbox a b \<noteq> {} \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i)"
   and "box a b \<noteq> {} \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i)"
   unfolding box_eq_empty[of a b] by fastforce+
 
 lemma
   fixes a :: "'a::euclidean_space"
   shows cbox_sing [simp]: "cbox a a = {a}"
     and box_sing [simp]: "box a a = {}"
   unfolding set_eq_iff mem_box eq_iff [symmetric]
   by (auto intro!: euclidean_eqI[where 'a='a])
      (metis all_not_in_conv nonempty_Basis)
 
 lemma subset_box_imp:
   fixes a :: "'a::euclidean_space"
   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"
     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"
     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"
      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"
   unfolding subset_eq[unfolded Ball_def] unfolding mem_box
   by (best intro: order_trans less_le_trans le_less_trans less_imp_le)+
 
 lemma box_subset_cbox:
   fixes a :: "'a::euclidean_space"
   shows "box a b \<subseteq> cbox a b"
   unfolding subset_eq [unfolded Ball_def] mem_box
   by (fast intro: less_imp_le)
 
 lemma subset_box:
   fixes a :: "'a::euclidean_space"
   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)
     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)
     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)
     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)
 proof -
   let ?lesscd = "\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i"
   let ?lerhs = "\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i"
   show ?th1 ?th2
     by (fastforce simp: mem_box)+
   have acdb: "a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i"
     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
   proof -
     have "box c d \<noteq> {}"
       using that
       unfolding box_eq_empty by force
     { 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"
       assume *: "a\<bullet>i > c\<bullet>i"
       then have "c \<bullet> j < ?x \<bullet> j \<and> ?x \<bullet> j < d \<bullet> j" if "j \<in> Basis" for j
         using cd that by (fastforce simp add: i *)
       then have "?x \<in> box c d"
         unfolding mem_box by auto
       moreover have "?x \<notin> cbox a b"
         using i cd * by (force simp: mem_box)
       ultimately have False using box by auto
     }
     then have "a\<bullet>i \<le> c\<bullet>i" by force
     moreover
     { 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"
       assume *: "b\<bullet>i < d\<bullet>i"
       then have "d \<bullet> j > ?x \<bullet> j \<and> ?x \<bullet> j > c \<bullet> j" if "j \<in> Basis" for j
         using cd that by (fastforce simp add: i *)
       then have "?x \<in> box c d"
         unfolding mem_box by auto
       moreover have "?x \<notin> cbox a b"
         using i cd * by (force simp: mem_box)
       ultimately have False using box by auto
     }
     then have "b\<bullet>i \<ge> d\<bullet>i" by (rule ccontr) auto
     ultimately show ?thesis by auto
   qed
   show ?th3
     using acdb by (fastforce simp add: mem_box)
   have acdb': "a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i"
     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
       using box_subset_cbox[of a b] that acdb by auto
   show ?th4
     using acdb' by (fastforce simp add: mem_box)
 qed
 
 lemma eq_cbox: "cbox a b = cbox c d \<longleftrightarrow> cbox a b = {} \<and> cbox c d = {} \<or> a = c \<and> b = d"
       (is "?lhs = ?rhs")
 proof
   assume ?lhs
   then have "cbox a b \<subseteq> cbox c d" "cbox c d \<subseteq> cbox a b"
     by auto
   then show ?rhs
     by (force simp: subset_box box_eq_empty intro: antisym euclidean_eqI)
 next
   assume ?rhs
   then show ?lhs
     by force
 qed
 
 lemma eq_cbox_box [simp]: "cbox a b = box c d \<longleftrightarrow> cbox a b = {} \<and> box c d = {}"
   (is "?lhs \<longleftrightarrow> ?rhs")
 proof
   assume L: ?lhs
   then have "cbox a b \<subseteq> box c d" "box c d \<subseteq> cbox a b"
     by auto
   then show ?rhs
     apply (simp add: subset_box)
     using L box_ne_empty box_sing apply (fastforce simp add:)
     done
 qed force
 
 lemma eq_box_cbox [simp]: "box a b = cbox c d \<longleftrightarrow> box a b = {} \<and> cbox c d = {}"
   by (metis eq_cbox_box)
 
 lemma eq_box: "box a b = box c d \<longleftrightarrow> box a b = {} \<and> box c d = {} \<or> a = c \<and> b = d"
   (is "?lhs \<longleftrightarrow> ?rhs")
 proof
   assume L: ?lhs
   then have "box a b \<subseteq> box c d" "box c d \<subseteq> box a b"
     by auto
   then show ?rhs
     apply (simp add: subset_box)
     using box_ne_empty(2) L
     apply auto
      apply (meson euclidean_eqI less_eq_real_def not_less)+
     done
 qed force
 
 lemma subset_box_complex:
    "cbox a b \<subseteq> cbox c d \<longleftrightarrow>
       (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"
    "cbox a b \<subseteq> box c d \<longleftrightarrow>
       (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"
    "box a b \<subseteq> cbox c d \<longleftrightarrow>
       (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"
    "box a b \<subseteq> box c d \<longleftrightarrow>
       (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"
   by (subst subset_box; force simp: Basis_complex_def)+
 
 lemma in_cbox_complex_iff:
   "x \<in> cbox a b \<longleftrightarrow> Re x \<in> {Re a..Re b} \<and> Im x \<in> {Im a..Im b}"
   by (cases x; cases a; cases b) (auto simp: cbox_Complex_eq)
 
 lemma box_Complex_eq:
   "box (Complex a c) (Complex b d) = (\<lambda>(x,y). Complex x y) ` (box a b \<times> box c d)"
   by (auto simp: box_def Basis_complex_def image_iff complex_eq_iff)
 
 lemma in_box_complex_iff:
   "x \<in> box a b \<longleftrightarrow> Re x \<in> {Re a<..<Re b} \<and> Im x \<in> {Im a<..<Im b}"
   by (cases x; cases a; cases b) (auto simp: box_Complex_eq)
 
 lemma Int_interval:
   fixes a :: "'a::euclidean_space"
   shows "cbox a b \<inter> cbox c d =
     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)"
   unfolding set_eq_iff and Int_iff and mem_box
   by auto
 
 lemma disjoint_interval:
   fixes a::"'a::euclidean_space"
   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)
     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)
     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)
     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)
 proof -
   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"
   have **: "\<And>P Q. (\<And>i :: 'a. i \<in> Basis \<Longrightarrow> Q ?z i \<Longrightarrow> P i) \<Longrightarrow>
       (\<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)"
     by blast
   note * = set_eq_iff Int_iff empty_iff mem_box ball_conj_distrib[symmetric] eq_False ball_simps(10)
   show ?th1 unfolding * by (intro **) auto
   show ?th2 unfolding * by (intro **) auto
   show ?th3 unfolding * by (intro **) auto
   show ?th4 unfolding * by (intro **) auto
 qed
 
 lemma UN_box_eq_UNIV: "(\<Union>i::nat. box (- (real i *\<^sub>R One)) (real i *\<^sub>R One)) = UNIV"
 proof -
   have "\<bar>x \<bullet> b\<bar> < real_of_int (\<lceil>Max ((\<lambda>b. \<bar>x \<bullet> b\<bar>)`Basis)\<rceil> + 1)"
     if [simp]: "b \<in> Basis" for x b :: 'a
   proof -
     have "\<bar>x \<bullet> b\<bar> \<le> real_of_int \<lceil>\<bar>x \<bullet> b\<bar>\<rceil>"
       by (rule le_of_int_ceiling)
     also have "\<dots> \<le> real_of_int \<lceil>Max ((\<lambda>b. \<bar>x \<bullet> b\<bar>)`Basis)\<rceil>"
       by (auto intro!: ceiling_mono)
     also have "\<dots> < real_of_int (\<lceil>Max ((\<lambda>b. \<bar>x \<bullet> b\<bar>)`Basis)\<rceil> + 1)"
       by simp
     finally show ?thesis .
   qed
   then have "\<exists>n::nat. \<forall>b\<in>Basis. \<bar>x \<bullet> b\<bar> < real n" for x :: 'a
     by (metis order.strict_trans reals_Archimedean2)
   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"
     by auto
   ultimately show ?thesis
     by (auto simp: box_def inner_sum_left inner_Basis sum.If_cases)
 qed
 
 lemma image_affinity_cbox: fixes m::real
   fixes a b c :: "'a::euclidean_space"
   shows "(\<lambda>x. m *\<^sub>R x + c) ` cbox a b =
     (if cbox a b = {} then {}
      else (if 0 \<le> m then cbox (m *\<^sub>R a + c) (m *\<^sub>R b + c)
      else cbox (m *\<^sub>R b + c) (m *\<^sub>R a + c)))"
 proof (cases "m = 0")
   case True
   {
     fix x
     assume "\<forall>i\<in>Basis. x \<bullet> i \<le> c \<bullet> i" "\<forall>i\<in>Basis. c \<bullet> i \<le> x \<bullet> i"
     then have "x = c"
       by (simp add: dual_order.antisym euclidean_eqI)
   }
   moreover have "c \<in> cbox (m *\<^sub>R a + c) (m *\<^sub>R b + c)"
     unfolding True by (auto)
   ultimately show ?thesis using True by (auto simp: cbox_def)
 next
   case False
   {
     fix y
     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"
     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"
       by (auto simp: inner_distrib)
   }
   moreover
   {
     fix y
     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"
     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"
       by (auto simp: mult_left_mono_neg inner_distrib)
   }
   moreover
   {
     fix y
     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"
     then have "y \<in> (\<lambda>x. m *\<^sub>R x + c) ` cbox a b"
       unfolding image_iff Bex_def mem_box
       apply (intro exI[where x="(1 / m) *\<^sub>R (y - c)"])
       apply (auto simp: pos_le_divide_eq pos_divide_le_eq mult.commute inner_distrib inner_diff_left)
       done
   }
   moreover
   {
     fix y
     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"
     then have "y \<in> (\<lambda>x. m *\<^sub>R x + c) ` cbox a b"
       unfolding image_iff Bex_def mem_box
       apply (intro exI[where x="(1 / m) *\<^sub>R (y - c)"])
       apply (auto simp: neg_le_divide_eq neg_divide_le_eq mult.commute inner_distrib inner_diff_left)
       done
   }
   ultimately show ?thesis using False by (auto simp: cbox_def)
 qed
 
 lemma image_smult_cbox:"(\<lambda>x. m *\<^sub>R (x::_::euclidean_space)) ` cbox a b =
   (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))"
   using image_affinity_cbox[of m 0 a b] by auto
 
 lemma swap_continuous:
   assumes "continuous_on (cbox (a,c) (b,d)) (\<lambda>(x,y). f x y)"
     shows "continuous_on (cbox (c,a) (d,b)) (\<lambda>(x, y). f y x)"
 proof -
   have "(\<lambda>(x, y). f y x) = (\<lambda>(x, y). f x y) \<circ> prod.swap"
     by auto
   then show ?thesis
     apply (rule ssubst)
     apply (rule continuous_on_compose)
     apply (simp add: split_def)
     apply (rule continuous_intros | simp add: assms)+
     done
 qed
 
 
 subsection \<open>General Intervals\<close>
 
 definition\<^marker>\<open>tag important\<close> "is_interval (s::('a::euclidean_space) set) \<longleftrightarrow>
   (\<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)"
 
 lemma is_interval_1:
   "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)"
   unfolding is_interval_def by auto
 
 lemma is_interval_Int: "is_interval X \<Longrightarrow> is_interval Y \<Longrightarrow> is_interval (X \<inter> Y)"
   unfolding is_interval_def
   by blast
 
 lemma is_interval_cbox [simp]: "is_interval (cbox a (b::'a::euclidean_space))" (is ?th1)
   and is_interval_box [simp]: "is_interval (box a b)" (is ?th2)
   unfolding is_interval_def mem_box Ball_def atLeastAtMost_iff
   by (meson order_trans le_less_trans less_le_trans less_trans)+
 
 lemma is_interval_empty [iff]: "is_interval {}"
   unfolding is_interval_def  by simp
 
 lemma is_interval_univ [iff]: "is_interval UNIV"
   unfolding is_interval_def  by simp
 
 lemma mem_is_intervalI:
   assumes "is_interval s"
     and "a \<in> s" "b \<in> s"
     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"
   shows "x \<in> s"
   by (rule assms(1)[simplified is_interval_def, rule_format, OF assms(2,3,4)])
 
 lemma interval_subst:
   fixes S::"'a::euclidean_space set"
   assumes "is_interval S"
     and "x \<in> S" "y j \<in> S"
     and "j \<in> Basis"
   shows "(\<Sum>i\<in>Basis. (if i = j then y i \<bullet> i else x \<bullet> i) *\<^sub>R i) \<in> S"
   by (rule mem_is_intervalI[OF assms(1,2)]) (auto simp: assms)
 
 lemma mem_box_componentwiseI:
   fixes S::"'a::euclidean_space set"
   assumes "is_interval S"
   assumes "\<And>i. i \<in> Basis \<Longrightarrow> x \<bullet> i \<in> ((\<lambda>x. x \<bullet> i) ` S)"
   shows "x \<in> S"
 proof -
   from assms have "\<forall>i \<in> Basis. \<exists>s \<in> S. x \<bullet> i = s \<bullet> i"
     by auto
   with finite_Basis obtain s and bs::"'a list"
     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"
       and bs: "set bs = Basis" "distinct bs"
     by (metis finite_distinct_list)
   from nonempty_Basis s obtain j where j: "j \<in> Basis" "s j \<in> S"
     by blast
   define y where
     "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))"
   have "x = (\<Sum>i\<in>Basis. (if i \<in> set bs then s i \<bullet> i else s j \<bullet> i) *\<^sub>R i)"
     using bs by (auto simp: s(1)[symmetric] euclidean_representation)
   also have [symmetric]: "y bs = \<dots>"
     using bs(2) bs(1)[THEN equalityD1]
     by (induct bs) (auto simp: y_def euclidean_representation intro!: euclidean_eqI[where 'a='a])
   also have "y bs \<in> S"
     using bs(1)[THEN equalityD1]
     apply (induct bs)
      apply (auto simp: y_def j)
     apply (rule interval_subst[OF assms(1)])
       apply (auto simp: s)
     done
   finally show ?thesis .
 qed
 
 lemma cbox01_nonempty [simp]: "cbox 0 One \<noteq> {}"
   by (simp add: box_ne_empty inner_Basis inner_sum_left sum_nonneg)
 
 lemma box01_nonempty [simp]: "box 0 One \<noteq> {}"
   by (simp add: box_ne_empty inner_Basis inner_sum_left)
 
 lemma empty_as_interval: "{} = cbox One (0::'a::euclidean_space)"
   using nonempty_Basis box01_nonempty box_eq_empty(1) box_ne_empty(1) by blast
 
 lemma interval_subset_is_interval:
   assumes "is_interval S"
   shows "cbox a b \<subseteq> S \<longleftrightarrow> cbox a b = {} \<or> a \<in> S \<and> b \<in> S" (is "?lhs = ?rhs")
 proof
   assume ?lhs
   then show ?rhs  using box_ne_empty(1) mem_box(2) by fastforce
 next
   assume ?rhs
   have "cbox a b \<subseteq> S" if "a \<in> S" "b \<in> S"
     using assms unfolding is_interval_def
     apply (clarsimp simp add: mem_box)
     using that by blast
   with \<open>?rhs\<close> show ?lhs
     by blast
 qed
 
 lemma is_real_interval_union:
   "is_interval (X \<union> Y)"
   if X: "is_interval X" and Y: "is_interval Y" and I: "(X \<noteq> {} \<Longrightarrow> Y \<noteq> {} \<Longrightarrow> X \<inter> Y \<noteq> {})"
   for X Y::"real set"
 proof -
   consider "X \<noteq> {}" "Y \<noteq> {}" | "X = {}" | "Y = {}" by blast
   then show ?thesis
   proof cases
     case 1
     then obtain r where "r \<in> X \<or> X \<inter> Y = {}" "r \<in> Y \<or> X \<inter> Y = {}"
       by blast
     then show ?thesis
       using I 1 X Y unfolding is_interval_1
       by (metis (full_types) Un_iff le_cases)
   qed (use that in auto)
 qed
 
 lemma is_interval_translationI:
   assumes "is_interval X"
   shows "is_interval ((+) x ` X)"
   unfolding is_interval_def
 proof safe
   fix b d e
   assume "b \<in> X" "d \<in> X"
     "\<forall>i\<in>Basis. (x + b) \<bullet> i \<le> e \<bullet> i \<and> e \<bullet> i \<le> (x + d) \<bullet> i \<or>
        (x + d) \<bullet> i \<le> e \<bullet> i \<and> e \<bullet> i \<le> (x + b) \<bullet> i"
   hence "e - x \<in> X"
     by (intro mem_is_intervalI[OF assms \<open>b \<in> X\<close> \<open>d \<in> X\<close>, of "e - x"])
       (auto simp: algebra_simps)
   thus "e \<in> (+) x ` X" by force
 qed
 
 lemma is_interval_uminusI:
   assumes "is_interval X"
   shows "is_interval (uminus ` X)"
   unfolding is_interval_def
 proof safe
   fix b d e
   assume "b \<in> X" "d \<in> X"
     "\<forall>i\<in>Basis. (- b) \<bullet> i \<le> e \<bullet> i \<and> e \<bullet> i \<le> (- d) \<bullet> i \<or>
        (- d) \<bullet> i \<le> e \<bullet> i \<and> e \<bullet> i \<le> (- b) \<bullet> i"
   hence "- e \<in> X"
     by (intro mem_is_intervalI[OF assms \<open>b \<in> X\<close> \<open>d \<in> X\<close>, of "- e"])
       (auto simp: algebra_simps)
   thus "e \<in> uminus ` X" by force
 qed
 
 lemma is_interval_uminus[simp]: "is_interval (uminus ` x) = is_interval x"
   using is_interval_uminusI[of x] is_interval_uminusI[of "uminus ` x"]
   by (auto simp: image_image)
 
 lemma is_interval_neg_translationI:
   assumes "is_interval X"
   shows "is_interval ((-) x ` X)"
 proof -
   have "(-) x ` X = (+) x ` uminus ` X"
     by (force simp: algebra_simps)
   also have "is_interval \<dots>"
     by (metis is_interval_uminusI is_interval_translationI assms)
   finally show ?thesis .
 qed
 
 lemma is_interval_translation[simp]:
   "is_interval ((+) x ` X) = is_interval X"
   using is_interval_neg_translationI[of "(+) x ` X" x]
   by (auto intro!: is_interval_translationI simp: image_image)
 
 lemma is_interval_minus_translation[simp]:
   shows "is_interval ((-) x ` X) = is_interval X"
 proof -
   have "(-) x ` X = (+) x ` uminus ` X"
     by (force simp: algebra_simps)
   also have "is_interval \<dots> = is_interval X"
     by simp
   finally show ?thesis .
 qed
 
 lemma is_interval_minus_translation'[simp]:
   shows "is_interval ((\<lambda>x. x - c) ` X) = is_interval X"
   using is_interval_translation[of "-c" X]
   by (metis image_cong uminus_add_conv_diff)
 
 lemma is_interval_cball_1[intro, simp]: "is_interval (cball a b)" for a b::real
   by (simp add: cball_eq_atLeastAtMost is_interval_def)
 
 lemma is_interval_ball_real: "is_interval (ball a b)" for a b::real
   by (simp add: ball_eq_greaterThanLessThan is_interval_def)
 
 
 subsection\<^marker>\<open>tag unimportant\<close> \<open>Bounded Projections\<close>
 
 lemma bounded_inner_imp_bdd_above:
   assumes "bounded s"
     shows "bdd_above ((\<lambda>x. x \<bullet> a) ` s)"
 by (simp add: assms bounded_imp_bdd_above bounded_linear_image bounded_linear_inner_left)
 
 lemma bounded_inner_imp_bdd_below:
   assumes "bounded s"
     shows "bdd_below ((\<lambda>x. x \<bullet> a) ` s)"
 by (simp add: assms bounded_imp_bdd_below bounded_linear_image bounded_linear_inner_left)
 
 
 subsection\<^marker>\<open>tag unimportant\<close> \<open>Structural rules for pointwise continuity\<close>
 
 lemma continuous_infnorm[continuous_intros]:
   "continuous F f \<Longrightarrow> continuous F (\<lambda>x. infnorm (f x))"
   unfolding continuous_def by (rule tendsto_infnorm)
 
 lemma continuous_inner[continuous_intros]:
   assumes "continuous F f"
     and "continuous F g"
   shows "continuous F (\<lambda>x. inner (f x) (g x))"
   using assms unfolding continuous_def by (rule tendsto_inner)
 
 
 subsection\<^marker>\<open>tag unimportant\<close> \<open>Structural rules for setwise continuity\<close>
 
 lemma continuous_on_infnorm[continuous_intros]:
   "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. infnorm (f x))"
   unfolding continuous_on by (fast intro: tendsto_infnorm)
 
 lemma continuous_on_inner[continuous_intros]:
   fixes g :: "'a::topological_space \<Rightarrow> 'b::real_inner"
   assumes "continuous_on s f"
     and "continuous_on s g"
   shows "continuous_on s (\<lambda>x. inner (f x) (g x))"
   using bounded_bilinear_inner assms
   by (rule bounded_bilinear.continuous_on)
 
 
 subsection\<^marker>\<open>tag unimportant\<close> \<open>Openness of halfspaces.\<close>
 
 lemma open_halfspace_lt: "open {x. inner a x < b}"
   by (simp add: open_Collect_less continuous_on_inner)
 
 lemma open_halfspace_gt: "open {x. inner a x > b}"
   by (simp add: open_Collect_less continuous_on_inner)
 
 lemma open_halfspace_component_lt: "open {x::'a::euclidean_space. x\<bullet>i < a}"
   by (simp add: open_Collect_less continuous_on_inner)
 
 lemma open_halfspace_component_gt: "open {x::'a::euclidean_space. x\<bullet>i > a}"
   by (simp add: open_Collect_less continuous_on_inner)
 
 lemma eucl_less_eq_halfspaces:
   fixes a :: "'a::euclidean_space"
   shows "{x. x <e a} = (\<Inter>i\<in>Basis. {x. x \<bullet> i < a \<bullet> i})"
         "{x. a <e x} = (\<Inter>i\<in>Basis. {x. a \<bullet> i < x \<bullet> i})"
   by (auto simp: eucl_less_def)
 
 lemma open_Collect_eucl_less[simp, intro]:
   fixes a :: "'a::euclidean_space"
   shows "open {x. x <e a}" "open {x. a <e x}"
   by (auto simp: eucl_less_eq_halfspaces open_halfspace_component_lt open_halfspace_component_gt)
 
 subsection\<^marker>\<open>tag unimportant\<close> \<open>Closure and Interior of halfspaces and hyperplanes\<close>
 
 lemma continuous_at_inner: "continuous (at x) (inner a)"
   unfolding continuous_at by (intro tendsto_intros)
 
 lemma closed_halfspace_le: "closed {x. inner a x \<le> b}"
   by (simp add: closed_Collect_le continuous_on_inner)
 
 lemma closed_halfspace_ge: "closed {x. inner a x \<ge> b}"
   by (simp add: closed_Collect_le continuous_on_inner)
 
 lemma closed_hyperplane: "closed {x. inner a x = b}"
   by (simp add: closed_Collect_eq continuous_on_inner)
 
 lemma closed_halfspace_component_le: "closed {x::'a::euclidean_space. x\<bullet>i \<le> a}"
   by (simp add: closed_Collect_le continuous_on_inner)
 
 lemma closed_halfspace_component_ge: "closed {x::'a::euclidean_space. x\<bullet>i \<ge> a}"
   by (simp add: closed_Collect_le continuous_on_inner)
 
 lemma closed_interval_left:
   fixes b :: "'a::euclidean_space"
   shows "closed {x::'a. \<forall>i\<in>Basis. x\<bullet>i \<le> b\<bullet>i}"
   by (simp add: Collect_ball_eq closed_INT closed_Collect_le continuous_on_inner)
 
 lemma closed_interval_right:
   fixes a :: "'a::euclidean_space"
   shows "closed {x::'a. \<forall>i\<in>Basis. a\<bullet>i \<le> x\<bullet>i}"
   by (simp add: Collect_ball_eq closed_INT closed_Collect_le continuous_on_inner)
 
 lemma interior_halfspace_le [simp]:
   assumes "a \<noteq> 0"
     shows "interior {x. a \<bullet> x \<le> b} = {x. a \<bullet> x < b}"
 proof -
   have *: "a \<bullet> x < b" if x: "x \<in> S" and S: "S \<subseteq> {x. a \<bullet> x \<le> b}" and "open S" for S x
   proof -
     obtain e where "e>0" and e: "cball x e \<subseteq> S"
       using \<open>open S\<close> open_contains_cball x by blast
     then have "x + (e / norm a) *\<^sub>R a \<in> cball x e"
       by (simp add: dist_norm)
     then have "x + (e / norm a) *\<^sub>R a \<in> S"
       using e by blast
     then have "x + (e / norm a) *\<^sub>R a \<in> {x. a \<bullet> x \<le> b}"
       using S by blast
     moreover have "e * (a \<bullet> a) / norm a > 0"
       by (simp add: \<open>0 < e\<close> assms)
     ultimately show ?thesis
       by (simp add: algebra_simps)
   qed
   show ?thesis
     by (rule interior_unique) (auto simp: open_halfspace_lt *)
 qed
 
 lemma interior_halfspace_ge [simp]:
    "a \<noteq> 0 \<Longrightarrow> interior {x. a \<bullet> x \<ge> b} = {x. a \<bullet> x > b}"
 using interior_halfspace_le [of "-a" "-b"] by simp
 
 lemma closure_halfspace_lt [simp]:
   assumes "a \<noteq> 0"
     shows "closure {x. a \<bullet> x < b} = {x. a \<bullet> x \<le> b}"
 proof -
   have [simp]: "-{x. a \<bullet> x < b} = {x. a \<bullet> x \<ge> b}"
     by (force simp:)
   then show ?thesis
     using interior_halfspace_ge [of a b] assms
     by (force simp: closure_interior)
 qed
 
 lemma closure_halfspace_gt [simp]:
    "a \<noteq> 0 \<Longrightarrow> closure {x. a \<bullet> x > b} = {x. a \<bullet> x \<ge> b}"
 using closure_halfspace_lt [of "-a" "-b"] by simp
 
 lemma interior_hyperplane [simp]:
   assumes "a \<noteq> 0"
     shows "interior {x. a \<bullet> x = b} = {}"
 proof -
   have [simp]: "{x. a \<bullet> x = b} = {x. a \<bullet> x \<le> b} \<inter> {x. a \<bullet> x \<ge> b}"
     by (force simp:)
   then show ?thesis
     by (auto simp: assms)
 qed
 
 lemma frontier_halfspace_le:
   assumes "a \<noteq> 0 \<or> b \<noteq> 0"
     shows "frontier {x. a \<bullet> x \<le> b} = {x. a \<bullet> x = b}"
 proof (cases "a = 0")
   case True with assms show ?thesis by simp
 next
   case False then show ?thesis
     by (force simp: frontier_def closed_halfspace_le)
 qed
 
 lemma frontier_halfspace_ge:
   assumes "a \<noteq> 0 \<or> b \<noteq> 0"
     shows "frontier {x. a \<bullet> x \<ge> b} = {x. a \<bullet> x = b}"
 proof (cases "a = 0")
   case True with assms show ?thesis by simp
 next
   case False then show ?thesis
     by (force simp: frontier_def closed_halfspace_ge)
 qed
 
 lemma frontier_halfspace_lt:
   assumes "a \<noteq> 0 \<or> b \<noteq> 0"
     shows "frontier {x. a \<bullet> x < b} = {x. a \<bullet> x = b}"
 proof (cases "a = 0")
   case True with assms show ?thesis by simp
 next
   case False then show ?thesis
     by (force simp: frontier_def interior_open open_halfspace_lt)
 qed
 
 lemma frontier_halfspace_gt:
   assumes "a \<noteq> 0 \<or> b \<noteq> 0"
     shows "frontier {x. a \<bullet> x > b} = {x. a \<bullet> x = b}"
 proof (cases "a = 0")
   case True with assms show ?thesis by simp
 next
   case False then show ?thesis
     by (force simp: frontier_def interior_open open_halfspace_gt)
 qed
 
 subsection\<^marker>\<open>tag unimportant\<close>\<open>Some more convenient intermediate-value theorem formulations\<close>
 
 lemma connected_ivt_hyperplane:
   assumes "connected S" and xy: "x \<in> S" "y \<in> S" and b: "inner a x \<le> b" "b \<le> inner a y"
   shows "\<exists>z \<in> S. inner a z = b"
 proof (rule ccontr)
   assume as:"\<not> (\<exists>z\<in>S. inner a z = b)"
   let ?A = "{x. inner a x < b}"
   let ?B = "{x. inner a x > b}"
   have "open ?A" "open ?B"
     using open_halfspace_lt and open_halfspace_gt by auto
   moreover have "?A \<inter> ?B = {}" by auto
   moreover have "S \<subseteq> ?A \<union> ?B" using as by auto
   ultimately show False
     using \<open>connected S\<close>[unfolded connected_def not_ex,
       THEN spec[where x="?A"], THEN spec[where x="?B"]]
     using xy b by auto
 qed
 
 lemma connected_ivt_component:
   fixes x::"'a::euclidean_space"
   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)"
   using connected_ivt_hyperplane[of S x y "k::'a" a]
   by (auto simp: inner_commute)
 
 
 subsection \<open>Limit Component Bounds\<close>
 
 lemma Lim_component_le:
   fixes f :: "'a \<Rightarrow> 'b::euclidean_space"
   assumes "(f \<longlongrightarrow> l) net"
     and "\<not> (trivial_limit net)"
     and "eventually (\<lambda>x. f(x)\<bullet>i \<le> b) net"
   shows "l\<bullet>i \<le> b"
   by (rule tendsto_le[OF assms(2) tendsto_const tendsto_inner[OF assms(1) tendsto_const] assms(3)])
 
 lemma Lim_component_ge:
   fixes f :: "'a \<Rightarrow> 'b::euclidean_space"
   assumes "(f \<longlongrightarrow> l) net"
     and "\<not> (trivial_limit net)"
     and "eventually (\<lambda>x. b \<le> (f x)\<bullet>i) net"
   shows "b \<le> l\<bullet>i"
   by (rule tendsto_le[OF assms(2) tendsto_inner[OF assms(1) tendsto_const] tendsto_const assms(3)])
 
 lemma Lim_component_eq:
   fixes f :: "'a \<Rightarrow> 'b::euclidean_space"
   assumes net: "(f \<longlongrightarrow> l) net" "\<not> trivial_limit net"
     and ev:"eventually (\<lambda>x. f(x)\<bullet>i = b) net"
   shows "l\<bullet>i = b"
   using ev[unfolded order_eq_iff eventually_conj_iff]
   using Lim_component_ge[OF net, of b i]
   using Lim_component_le[OF net, of i b]
   by auto
 
 lemma open_box[intro]: "open (box a b)"
 proof -
   have "open (\<Inter>i\<in>Basis. ((\<bullet>) i) -` {a \<bullet> i <..< b \<bullet> i})"
     by (auto intro!: continuous_open_vimage continuous_inner continuous_ident continuous_const)
   also have "(\<Inter>i\<in>Basis. ((\<bullet>) i) -` {a \<bullet> i <..< b \<bullet> i}) = box a b"
     by (auto simp: box_def inner_commute)
   finally show ?thesis .
 qed
 
 lemma closed_cbox[intro]:
   fixes a b :: "'a::euclidean_space"
   shows "closed (cbox a b)"
 proof -
   have "closed (\<Inter>i\<in>Basis. (\<lambda>x. x\<bullet>i) -` {a\<bullet>i .. b\<bullet>i})"
     by (intro closed_INT ballI continuous_closed_vimage allI
       linear_continuous_at closed_real_atLeastAtMost finite_Basis bounded_linear_inner_left)
   also have "(\<Inter>i\<in>Basis. (\<lambda>x. x\<bullet>i) -` {a\<bullet>i .. b\<bullet>i}) = cbox a b"
     by (auto simp: cbox_def)
   finally show "closed (cbox a b)" .
 qed
 
 lemma interior_cbox [simp]:
   fixes a b :: "'a::euclidean_space"
   shows "interior (cbox a b) = box a b" (is "?L = ?R")
 proof(rule subset_antisym)
   show "?R \<subseteq> ?L"
     using box_subset_cbox open_box
     by (rule interior_maximal)
   {
     fix x
     assume "x \<in> interior (cbox a b)"
     then obtain s where s: "open s" "x \<in> s" "s \<subseteq> cbox a b" ..
     then obtain e where "e>0" and e:"\<forall>x'. dist x' x < e \<longrightarrow> x' \<in> cbox a b"
       unfolding open_dist and subset_eq by auto
     {
       fix i :: 'a
       assume i: "i \<in> Basis"
       have "dist (x - (e / 2) *\<^sub>R i) x < e"
         and "dist (x + (e / 2) *\<^sub>R i) x < e"
         unfolding dist_norm
         apply auto
         unfolding norm_minus_cancel
         using norm_Basis[OF i] \<open>e>0\<close>
         apply auto
         done
       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"
         using e[THEN spec[where x="x - (e/2) *\<^sub>R i"]]
           and e[THEN spec[where x="x + (e/2) *\<^sub>R i"]]
         unfolding mem_box
         using i
         by blast+
       then have "a \<bullet> i < x \<bullet> i" and "x \<bullet> i < b \<bullet> i"
         using \<open>e>0\<close> i
         by (auto simp: inner_diff_left inner_Basis inner_add_left)
     }
     then have "x \<in> box a b"
       unfolding mem_box by auto
   }
   then show "?L \<subseteq> ?R" ..
 qed
 
 lemma bounded_cbox [simp]:
   fixes a :: "'a::euclidean_space"
   shows "bounded (cbox a b)"
 proof -
   let ?b = "\<Sum>i\<in>Basis. \<bar>a\<bullet>i\<bar> + \<bar>b\<bullet>i\<bar>"
   {
     fix x :: "'a"
     assume "\<And>i. i\<in>Basis \<Longrightarrow> a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i"
     then have "(\<Sum>i\<in>Basis. \<bar>x \<bullet> i\<bar>) \<le> ?b"
       by (force simp: intro!: sum_mono)
     then have "norm x \<le> ?b"
       using norm_le_l1[of x] by auto
   }
   then show ?thesis
     unfolding cbox_def bounded_iff by force
 qed
 
 lemma bounded_box [simp]:
   fixes a :: "'a::euclidean_space"
   shows "bounded (box a b)"
   using bounded_cbox[of a b] box_subset_cbox[of a b] bounded_subset[of "cbox a b" "box a b"]
   by simp
 
 lemma not_interval_UNIV [simp]:
   fixes a :: "'a::euclidean_space"
   shows "cbox a b \<noteq> UNIV" "box a b \<noteq> UNIV"
   using bounded_box[of a b] bounded_cbox[of a b] by force+
 
 lemma not_interval_UNIV2 [simp]:
   fixes a :: "'a::euclidean_space"
   shows "UNIV \<noteq> cbox a b" "UNIV \<noteq> box a b"
   using bounded_box[of a b] bounded_cbox[of a b] by force+
 
 lemma box_midpoint:
   fixes a :: "'a::euclidean_space"
   assumes "box a b \<noteq> {}"
   shows "((1/2) *\<^sub>R (a + b)) \<in> box a b"
 proof -
   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
     using assms that by (auto simp: inner_add_left box_ne_empty)
   then show ?thesis unfolding mem_box by auto
 qed
 
 lemma open_cbox_convex:
   fixes x :: "'a::euclidean_space"
   assumes x: "x \<in> box a b"
     and y: "y \<in> cbox a b"
     and e: "0 < e" "e \<le> 1"
   shows "(e *\<^sub>R x + (1 - e) *\<^sub>R y) \<in> box a b"
 proof -
   {
     fix i :: 'a
     assume i: "i \<in> Basis"
     have "a \<bullet> i = e * (a \<bullet> i) + (1 - e) * (a \<bullet> i)"
       unfolding left_diff_distrib by simp
     also have "\<dots> < e * (x \<bullet> i) + (1 - e) * (y \<bullet> i)"
     proof (rule add_less_le_mono)
       show "e * (a \<bullet> i) < e * (x \<bullet> i)"
         using \<open>0 < e\<close> i mem_box(1) x by auto
       show "(1 - e) * (a \<bullet> i) \<le> (1 - e) * (y \<bullet> i)"
         by (meson diff_ge_0_iff_ge \<open>e \<le> 1\<close> i mem_box(2) mult_left_mono y)
     qed
     finally have "a \<bullet> i < (e *\<^sub>R x + (1 - e) *\<^sub>R y) \<bullet> i"
       unfolding inner_simps by auto
     moreover
     {
       have "b \<bullet> i = e * (b\<bullet>i) + (1 - e) * (b\<bullet>i)"
         unfolding left_diff_distrib by simp
       also have "\<dots> > e * (x \<bullet> i) + (1 - e) * (y \<bullet> i)"
       proof (rule add_less_le_mono)
         show "e * (x \<bullet> i) < e * (b \<bullet> i)"
           using \<open>0 < e\<close> i mem_box(1) x by auto
         show "(1 - e) * (y \<bullet> i) \<le> (1 - e) * (b \<bullet> i)"
           by (meson diff_ge_0_iff_ge \<open>e \<le> 1\<close> i mem_box(2) mult_left_mono y)
       qed
       finally have "(e *\<^sub>R x + (1 - e) *\<^sub>R y) \<bullet> i < b \<bullet> i"
         unfolding inner_simps by auto
     }
     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"
       by auto
   }
   then show ?thesis
     unfolding mem_box by auto
 qed
 
 lemma closure_cbox [simp]: "closure (cbox a b) = cbox a b"
   by (simp add: closed_cbox)
 
 lemma closure_box [simp]:
   fixes a :: "'a::euclidean_space"
    assumes "box a b \<noteq> {}"
   shows "closure (box a b) = cbox a b"
 proof -
   have ab: "a <e b"
     using assms by (simp add: eucl_less_def box_ne_empty)
   let ?c = "(1 / 2) *\<^sub>R (a + b)"
   {
     fix x
     assume as:"x \<in> cbox a b"
     define f where [abs_def]: "f n = x + (inverse (real n + 1)) *\<^sub>R (?c - x)" for n
     {
       fix n
       assume fn: "f n <e b \<longrightarrow> a <e f n \<longrightarrow> f n = x" and xc: "x \<noteq> ?c"
       have *: "0 < inverse (real n + 1)" "inverse (real n + 1) \<le> 1"
         unfolding inverse_le_1_iff by auto
       have "(inverse (real n + 1)) *\<^sub>R ((1 / 2) *\<^sub>R (a + b)) + (1 - inverse (real n + 1)) *\<^sub>R x =
         x + (inverse (real n + 1)) *\<^sub>R (((1 / 2) *\<^sub>R (a + b)) - x)"
         by (auto simp: algebra_simps)
       then have "f n <e b" and "a <e f n"
         using open_cbox_convex[OF box_midpoint[OF assms] as *]
         unfolding f_def by (auto simp: box_def eucl_less_def)
       then have False
         using fn unfolding f_def using xc by auto
     }
     moreover
     {
       assume "\<not> (f \<longlongrightarrow> x) sequentially"
       {
         fix e :: real
         assume "e > 0"
         then obtain N :: nat where N: "inverse (real (N + 1)) < e"
           using reals_Archimedean by auto
         have "inverse (real n + 1) < e" if "N \<le> n" for n
           by (auto intro!: that le_less_trans [OF _ N])
         then have "\<exists>N::nat. \<forall>n\<ge>N. inverse (real n + 1) < e" by auto
       }
       then have "((\<lambda>n. inverse (real n + 1)) \<longlongrightarrow> 0) sequentially"
         unfolding lim_sequentially by(auto simp: dist_norm)
       then have "(f \<longlongrightarrow> x) sequentially"
         unfolding f_def
         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]
         using tendsto_scaleR [OF _ tendsto_const, of "\<lambda>n::nat. inverse (real n + 1)" 0 sequentially "((1 / 2) *\<^sub>R (a + b) - x)"]
         by auto
     }
     ultimately have "x \<in> closure (box a b)"
       using as box_midpoint[OF assms]
       unfolding closure_def islimpt_sequential
       by (cases "x=?c") (auto simp: in_box_eucl_less)
   }
   then show ?thesis
     using closure_minimal[OF box_subset_cbox, of a b] by blast
 qed
 
 lemma bounded_subset_box_symmetric:
   fixes S :: "('a::euclidean_space) set"
   assumes "bounded S"
   obtains a where "S \<subseteq> box (-a) a"
 proof -
   obtain b where "b>0" and b: "\<forall>x\<in>S. norm x \<le> b"
     using assms[unfolded bounded_pos] by auto
   define a :: 'a where "a = (\<Sum>i\<in>Basis. (b + 1) *\<^sub>R i)"
   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
     using b Basis_le_norm[OF i, of x] that by (auto simp: a_def)
   then have "S \<subseteq> box (-a) a"
     by (auto simp: simp add: box_def)
   then show ?thesis ..
 qed
 
 lemma bounded_subset_cbox_symmetric:
   fixes S :: "('a::euclidean_space) set"
   assumes "bounded S"
   obtains a where "S \<subseteq> cbox (-a) a"
 proof -
   obtain a where "S \<subseteq> box (-a) a"
     using bounded_subset_box_symmetric[OF assms] by auto
   then show ?thesis
     by (meson box_subset_cbox dual_order.trans that)
 qed
 
 lemma frontier_cbox:
   fixes a b :: "'a::euclidean_space"
   shows "frontier (cbox a b) = cbox a b - box a b"
   unfolding frontier_def unfolding interior_cbox and closure_closed[OF closed_cbox] ..
 
 lemma frontier_box:
   fixes a b :: "'a::euclidean_space"
   shows "frontier (box a b) = (if box a b = {} then {} else cbox a b - box a b)"
 proof (cases "box a b = {}")
   case True
   then show ?thesis
     using frontier_empty by auto
 next
   case False
   then show ?thesis
     unfolding frontier_def and closure_box[OF False] and interior_open[OF open_box]
     by auto
 qed
 
 lemma Int_interval_mixed_eq_empty:
   fixes a :: "'a::euclidean_space"
    assumes "box c d \<noteq> {}"
   shows "box a b \<inter> cbox c d = {} \<longleftrightarrow> box a b \<inter> box c d = {}"
   unfolding closure_box[OF assms, symmetric]
   unfolding open_Int_closure_eq_empty[OF open_box] ..
 
 subsection \<open>Class Instances\<close>
 
 lemma compact_lemma:
   fixes f :: "nat \<Rightarrow> 'a::euclidean_space"
   assumes "bounded (range f)"
   shows "\<forall>d\<subseteq>Basis. \<exists>l::'a. \<exists> r.
     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)"
   by (rule compact_lemma_general[where unproj="\<lambda>e. \<Sum>i\<in>Basis. e i *\<^sub>R i"])
      (auto intro!: assms bounded_linear_inner_left bounded_linear_image
        simp: euclidean_representation)
 
 instance\<^marker>\<open>tag important\<close> euclidean_space \<subseteq> heine_borel
 proof
   fix f :: "nat \<Rightarrow> 'a"
   assume f: "bounded (range f)"
   then obtain l::'a and r where r: "strict_mono r"
     and l: "\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>Basis. dist (f (r n) \<bullet> i) (l \<bullet> i) < e) sequentially"
     using compact_lemma [OF f] by blast
   {
     fix e::real
     assume "e > 0"
     hence "e / real_of_nat DIM('a) > 0" by (simp)
     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"
       by simp
     moreover
     {
       fix n
       assume n: "\<forall>i\<in>Basis. dist (f (r n) \<bullet> i) (l \<bullet> i) < e / (real_of_nat DIM('a))"
       have "dist (f (r n)) l \<le> (\<Sum>i\<in>Basis. dist (f (r n) \<bullet> i) (l \<bullet> i))"
         apply (subst euclidean_dist_l2)
         using zero_le_dist
         apply (rule L2_set_le_sum)
         done
       also have "\<dots> < (\<Sum>i\<in>(Basis::'a set). e / (real_of_nat DIM('a)))"
         apply (rule sum_strict_mono)
         using n
         apply auto
         done
       finally have "dist (f (r n)) l < e"
         by auto
     }
     ultimately have "eventually (\<lambda>n. dist (f (r n)) l < e) sequentially"
       by (rule eventually_mono)
   }
   then have *: "((f \<circ> r) \<longlongrightarrow> l) sequentially"
     unfolding o_def tendsto_iff by simp
   with r show "\<exists>l r. strict_mono r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
     by auto
 qed
 
 instance\<^marker>\<open>tag important\<close> euclidean_space \<subseteq> banach ..
 
 instance euclidean_space \<subseteq> second_countable_topology
 proof
   define a where "a f = (\<Sum>i\<in>Basis. fst (f i) *\<^sub>R i)" for f :: "'a \<Rightarrow> real \<times> real"
   then have a: "\<And>f. (\<Sum>i\<in>Basis. fst (f i) *\<^sub>R i) = a f"
     by simp
   define b where "b f = (\<Sum>i\<in>Basis. snd (f i) *\<^sub>R i)" for f :: "'a \<Rightarrow> real \<times> real"
   then have b: "\<And>f. (\<Sum>i\<in>Basis. snd (f i) *\<^sub>R i) = b f"
     by simp
   define B where "B = (\<lambda>f. box (a f) (b f)) ` (Basis \<rightarrow>\<^sub>E (\<rat> \<times> \<rat>))"
 
   have "Ball B open" by (simp add: B_def open_box)
   moreover have "(\<forall>A. open A \<longrightarrow> (\<exists>B'\<subseteq>B. \<Union>B' = A))"
   proof safe
     fix A::"'a set"
     assume "open A"
     show "\<exists>B'\<subseteq>B. \<Union>B' = A"
       apply (rule exI[of _ "{b\<in>B. b \<subseteq> A}"])
       apply (subst (3) open_UNION_box[OF \<open>open A\<close>])
       apply (auto simp: a b B_def)
       done
   qed
   ultimately
   have "topological_basis B"
     unfolding topological_basis_def by blast
   moreover
   have "countable B"
     unfolding B_def
     by (intro countable_image countable_PiE finite_Basis countable_SIGMA countable_rat)
   ultimately show "\<exists>B::'a set set. countable B \<and> open = generate_topology B"
     by (blast intro: topological_basis_imp_subbasis)
 qed
 
 instance euclidean_space \<subseteq> polish_space ..
 
 
 subsection \<open>Compact Boxes\<close>
 
 lemma compact_cbox [simp]:
   fixes a :: "'a::euclidean_space"
   shows "compact (cbox a b)"
   using bounded_closed_imp_seq_compact[of "cbox a b"] using bounded_cbox[of a b]
   by (auto simp: compact_eq_seq_compact_metric)
 
 proposition is_interval_compact:
    "is_interval S \<and> compact S \<longleftrightarrow> (\<exists>a b. S = cbox a b)"   (is "?lhs = ?rhs")
 proof (cases "S = {}")
   case True
   with empty_as_interval show ?thesis by auto
 next
   case False
   show ?thesis
   proof
     assume L: ?lhs
     then have "is_interval S" "compact S" by auto
     define a where "a \<equiv> \<Sum>i\<in>Basis. (INF x\<in>S. x \<bullet> i) *\<^sub>R i"
     define b where "b \<equiv> \<Sum>i\<in>Basis. (SUP x\<in>S. x \<bullet> i) *\<^sub>R i"
     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"
       by (simp add: cInf_lower bounded_inner_imp_bdd_below compact_imp_bounded L)
     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)"
       by (simp add: cSup_upper bounded_inner_imp_bdd_above compact_imp_bounded L)
     have 3: "x \<in> S" if inf: "\<And>i. i \<in> Basis \<Longrightarrow> (INF x\<in>S. x \<bullet> i) \<le> x \<bullet> i"
                    and sup: "\<And>i. i \<in> Basis \<Longrightarrow> x \<bullet> i \<le> (SUP x\<in>S. x \<bullet> i)" for x
     proof (rule mem_box_componentwiseI [OF \<open>is_interval S\<close>])
       fix i::'a
       assume i: "i \<in> Basis"
       have cont: "continuous_on S (\<lambda>x. x \<bullet> i)"
         by (intro continuous_intros)
       obtain a where "a \<in> S" and a: "\<And>y. y\<in>S \<Longrightarrow> a \<bullet> i \<le> y \<bullet> i"
         using continuous_attains_inf [OF \<open>compact S\<close> False cont] by blast
       obtain b where "b \<in> S" and b: "\<And>y. y\<in>S \<Longrightarrow> y \<bullet> i \<le> b \<bullet> i"
         using continuous_attains_sup [OF \<open>compact S\<close> False cont] by blast
       have "a \<bullet> i \<le> (INF x\<in>S. x \<bullet> i)"
         by (simp add: False a cINF_greatest)
       also have "\<dots> \<le> x \<bullet> i"
         by (simp add: i inf)
       finally have ai: "a \<bullet> i \<le> x \<bullet> i" .
       have "x \<bullet> i \<le> (SUP x\<in>S. x \<bullet> i)"
         by (simp add: i sup)
       also have "(SUP x\<in>S. x \<bullet> i) \<le> b \<bullet> i"
         by (simp add: False b cSUP_least)
       finally have bi: "x \<bullet> i \<le> b \<bullet> i" .
       show "x \<bullet> i \<in> (\<lambda>x. x \<bullet> i) ` S"
         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)
         apply (simp add: i)
         apply (rule mem_is_intervalI [OF \<open>is_interval S\<close> \<open>a \<in> S\<close> \<open>b \<in> S\<close>])
         using i ai bi apply force
         done
     qed
     have "S = cbox a b"
       by (auto simp: a_def b_def mem_box intro: 1 2 3)
     then show ?rhs
       by blast
   next
     assume R: ?rhs
     then show ?lhs
       using compact_cbox is_interval_cbox by blast
   qed
 qed
 
 
 subsection\<^marker>\<open>tag unimportant\<close>\<open>Componentwise limits and continuity\<close>
 
 text\<open>But is the premise really necessary? Need to generalise @{thm euclidean_dist_l2}\<close>
 lemma Euclidean_dist_upper: "i \<in> Basis \<Longrightarrow> dist (x \<bullet> i) (y \<bullet> i) \<le> dist x y"
   by (metis (no_types) member_le_L2_set euclidean_dist_l2 finite_Basis)
 
 text\<open>But is the premise \<^term>\<open>i \<in> Basis\<close> really necessary?\<close>
 lemma open_preimage_inner:
   assumes "open S" "i \<in> Basis"
     shows "open {x. x \<bullet> i \<in> S}"
 proof (rule openI, simp)
   fix x
   assume x: "x \<bullet> i \<in> S"
   with assms obtain e where "0 < e" and e: "ball (x \<bullet> i) e \<subseteq> S"
     by (auto simp: open_contains_ball_eq)
   have "\<exists>e>0. ball (y \<bullet> i) e \<subseteq> S" if dxy: "dist x y < e / 2" for y
   proof (intro exI conjI)
     have "dist (x \<bullet> i) (y \<bullet> i) < e / 2"
       by (meson \<open>i \<in> Basis\<close> dual_order.trans Euclidean_dist_upper not_le that)
     then have "dist (x \<bullet> i) z < e" if "dist (y \<bullet> i) z < e / 2" for z
       by (metis dist_commute dist_triangle_half_l that)
     then have "ball (y \<bullet> i) (e / 2) \<subseteq> ball (x \<bullet> i) e"
       using mem_ball by blast
       with e show "ball (y \<bullet> i) (e / 2) \<subseteq> S"
         by (metis order_trans)
   qed (simp add: \<open>0 < e\<close>)
   then show "\<exists>e>0. ball x e \<subseteq> {s. s \<bullet> i \<in> S}"
     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)
 qed
 
 proposition tendsto_componentwise_iff:
   fixes f :: "_ \<Rightarrow> 'b::euclidean_space"
   shows "(f \<longlongrightarrow> l) F \<longleftrightarrow> (\<forall>i \<in> Basis. ((\<lambda>x. (f x \<bullet> i)) \<longlongrightarrow> (l \<bullet> i)) F)"
          (is "?lhs = ?rhs")
 proof
   assume ?lhs
   then show ?rhs
     unfolding tendsto_def
     apply clarify
     apply (drule_tac x="{s. s \<bullet> i \<in> S}" in spec)
     apply (auto simp: open_preimage_inner)
     done
 next
   assume R: ?rhs
   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"
     unfolding tendsto_iff by blast
   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"
       by (simp add: eventually_ball_finite_distrib [symmetric])
   show ?lhs
   unfolding tendsto_iff
   proof clarify
     fix e::real
     assume "0 < e"
     have *: "L2_set (\<lambda>i. dist (f x \<bullet> i) (l \<bullet> i)) Basis < e"
              if "\<forall>i\<in>Basis. dist (f x \<bullet> i) (l \<bullet> i) < e / real DIM('b)" for x
     proof -
       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"
         by (simp add: L2_set_le_sum)
       also have "... < DIM('b) * (e / real DIM('b))"
         apply (rule sum_bounded_above_strict)
         using that by auto
       also have "... = e"
         by (simp add: field_simps)
       finally show "L2_set (\<lambda>i. dist (f x \<bullet> i) (l \<bullet> i)) Basis < e" .
     qed
     have "\<forall>\<^sub>F x in F. \<forall>i\<in>Basis. dist (f x \<bullet> i) (l \<bullet> i) < e / DIM('b)"
       apply (rule R')
       using \<open>0 < e\<close> by simp
     then show "\<forall>\<^sub>F x in F. dist (f x) l < e"
       apply (rule eventually_mono)
       apply (subst euclidean_dist_l2)
       using * by blast
   qed
 qed
 
 
 corollary continuous_componentwise:
    "continuous F f \<longleftrightarrow> (\<forall>i \<in> Basis. continuous F (\<lambda>x. (f x \<bullet> i)))"
 by (simp add: continuous_def tendsto_componentwise_iff [symmetric])
 
 corollary continuous_on_componentwise:
   fixes S :: "'a :: t2_space set"
   shows "continuous_on S f \<longleftrightarrow> (\<forall>i \<in> Basis. continuous_on S (\<lambda>x. (f x \<bullet> i)))"
   apply (simp add: continuous_on_eq_continuous_within)
   using continuous_componentwise by blast
 
 lemma linear_componentwise_iff:
      "(linear f') \<longleftrightarrow> (\<forall>i\<in>Basis. linear (\<lambda>x. f' x \<bullet> i))"
   apply (auto simp: linear_iff inner_left_distrib)
    apply (metis inner_left_distrib euclidean_eq_iff)
   by (metis euclidean_eqI inner_scaleR_left)
 
 lemma bounded_linear_componentwise_iff:
      "(bounded_linear f') \<longleftrightarrow> (\<forall>i\<in>Basis. bounded_linear (\<lambda>x. f' x \<bullet> i))"
      (is "?lhs = ?rhs")
 proof
   assume ?lhs then show ?rhs
     by (simp add: bounded_linear_inner_left_comp)
 next
   assume ?rhs
   then have "(\<forall>i\<in>Basis. \<exists>K. \<forall>x. \<bar>f' x \<bullet> i\<bar> \<le> norm x * K)" "linear f'"
     by (auto simp: bounded_linear_def bounded_linear_axioms_def linear_componentwise_iff [symmetric] ball_conj_distrib)
   then obtain F where F: "\<And>i x. i \<in> Basis \<Longrightarrow> \<bar>f' x \<bullet> i\<bar> \<le> norm x * F i"
     by metis
   have "norm (f' x) \<le> norm x * sum F Basis" for x
   proof -
     have "norm (f' x) \<le> (\<Sum>i\<in>Basis. \<bar>f' x \<bullet> i\<bar>)"
       by (rule norm_le_l1)
     also have "... \<le> (\<Sum>i\<in>Basis. norm x * F i)"
       by (metis F sum_mono)
     also have "... = norm x * sum F Basis"
       by (simp add: sum_distrib_left)
     finally show ?thesis .
   qed
   then show ?lhs
     by (force simp: bounded_linear_def bounded_linear_axioms_def \<open>linear f'\<close>)
 qed
 
 subsection\<^marker>\<open>tag unimportant\<close> \<open>Continuous Extension\<close>
 
 definition clamp :: "'a::euclidean_space \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" where
   "clamp a b x = (if (\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i)
     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)
     else a)"
 
 lemma clamp_in_interval[simp]:
   assumes "\<And>i. i \<in> Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i"
   shows "clamp a b x \<in> cbox a b"
   unfolding clamp_def
   using box_ne_empty(1)[of a b] assms by (auto simp: cbox_def)
 
 lemma clamp_cancel_cbox[simp]:
   fixes x a b :: "'a::euclidean_space"
   assumes x: "x \<in> cbox a b"
   shows "clamp a b x = x"
   using assms
   by (auto simp: clamp_def mem_box intro!: euclidean_eqI[where 'a='a])
 
 lemma clamp_empty_interval:
   assumes "i \<in> Basis" "a \<bullet> i > b \<bullet> i"
   shows "clamp a b = (\<lambda>_. a)"
   using assms
   by (force simp: clamp_def[abs_def] split: if_splits intro!: ext)
 
 lemma dist_clamps_le_dist_args:
   fixes x :: "'a::euclidean_space"
   shows "dist (clamp a b y) (clamp a b x) \<le> dist y x"
 proof cases
   assume le: "(\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i)"
   then have "(\<Sum>i\<in>Basis. (dist (clamp a b y \<bullet> i) (clamp a b x \<bullet> i))\<^sup>2) \<le>
     (\<Sum>i\<in>Basis. (dist (y \<bullet> i) (x \<bullet> i))\<^sup>2)"
     by (auto intro!: sum_mono simp: clamp_def dist_real_def abs_le_square_iff[symmetric])
   then show ?thesis
     by (auto intro: real_sqrt_le_mono
       simp: euclidean_dist_l2[where y=x] euclidean_dist_l2[where y="clamp a b x"] L2_set_def)
 qed (auto simp: clamp_def)
 
 lemma clamp_continuous_at:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::metric_space"
     and x :: 'a
   assumes f_cont: "continuous_on (cbox a b) f"
   shows "continuous (at x) (\<lambda>x. f (clamp a b x))"
 proof cases
   assume le: "(\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i)"
   show ?thesis
     unfolding continuous_at_eps_delta
   proof safe
     fix x :: 'a
     fix e :: real
     assume "e > 0"
     moreover have "clamp a b x \<in> cbox a b"
       by (simp add: le)
     moreover note f_cont[simplified continuous_on_iff]
     ultimately
     obtain d where d: "0 < d"
       "\<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"
       by force
     show "\<exists>d>0. \<forall>x'. dist x' x < d \<longrightarrow>
       dist (f (clamp a b x')) (f (clamp a b x)) < e"
       using le
       by (auto intro!: d clamp_in_interval dist_clamps_le_dist_args[THEN le_less_trans])
   qed
 qed (auto simp: clamp_empty_interval)
 
 lemma clamp_continuous_on:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::metric_space"
   assumes f_cont: "continuous_on (cbox a b) f"
   shows "continuous_on S (\<lambda>x. f (clamp a b x))"
   using assms
   by (auto intro: continuous_at_imp_continuous_on clamp_continuous_at)
 
 lemma clamp_bounded:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::metric_space"
   assumes bounded: "bounded (f ` (cbox a b))"
   shows "bounded (range (\<lambda>x. f (clamp a b x)))"
 proof cases
   assume le: "(\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i)"
   from bounded obtain c where f_bound: "\<forall>x\<in>f ` cbox a b. dist undefined x \<le> c"
     by (auto simp: bounded_any_center[where a=undefined])
   then show ?thesis
     by (auto intro!: exI[where x=c] clamp_in_interval[OF le[rule_format]]
         simp: bounded_any_center[where a=undefined])
 qed (auto simp: clamp_empty_interval image_def)
 
 
 definition ext_cont :: "('a::euclidean_space \<Rightarrow> 'b::metric_space) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b"
   where "ext_cont f a b = (\<lambda>x. f (clamp a b x))"
 
 lemma ext_cont_cancel_cbox[simp]:
   fixes x a b :: "'a::euclidean_space"
   assumes x: "x \<in> cbox a b"
   shows "ext_cont f a b x = f x"
   using assms
   unfolding ext_cont_def
   by (auto simp: clamp_def mem_box intro!: euclidean_eqI[where 'a='a] arg_cong[where f=f])
 
 lemma continuous_on_ext_cont[continuous_intros]:
   "continuous_on (cbox a b) f \<Longrightarrow> continuous_on S (ext_cont f a b)"
   by (auto intro!: clamp_continuous_on simp: ext_cont_def)
 
 
 subsection \<open>Separability\<close>
 
 lemma univ_second_countable_sequence:
   obtains B :: "nat \<Rightarrow> 'a::euclidean_space set"
     where "inj B" "\<And>n. open(B n)" "\<And>S. open S \<Longrightarrow> \<exists>k. S = \<Union>{B n |n. n \<in> k}"
 proof -
   obtain \<B> :: "'a set set"
   where "countable \<B>"
     and opn: "\<And>C. C \<in> \<B> \<Longrightarrow> open C"
     and Un: "\<And>S. open S \<Longrightarrow> \<exists>U. U \<subseteq> \<B> \<and> S = \<Union>U"
     using univ_second_countable by blast
   have *: "infinite (range (\<lambda>n. ball (0::'a) (inverse(Suc n))))"
     apply (rule Infinite_Set.range_inj_infinite)
     apply (simp add: inj_on_def ball_eq_ball_iff)
     done
   have "infinite \<B>"
   proof
     assume "finite \<B>"
     then have "finite (Union ` (Pow \<B>))"
       by simp
     then have "finite (range (\<lambda>n. ball (0::'a) (inverse(Suc n))))"
       apply (rule rev_finite_subset)
       by (metis (no_types, lifting) PowI image_eqI image_subset_iff Un [OF open_ball])
     with * show False by simp
   qed
   obtain f :: "nat \<Rightarrow> 'a set" where "\<B> = range f" "inj f"
     by (blast intro: countable_as_injective_image [OF \<open>countable \<B>\<close> \<open>infinite \<B>\<close>])
   have *: "\<exists>k. S = \<Union>{f n |n. n \<in> k}" if "open S" for S
     using Un [OF that]
     apply clarify
     apply (rule_tac x="f-`U" in exI)
     using \<open>inj f\<close> \<open>\<B> = range f\<close> apply force
     done
   show ?thesis
     apply (rule that [OF \<open>inj f\<close> _ *])
     apply (auto simp: \<open>\<B> = range f\<close> opn)
     done
 qed
 
 proposition separable:
   fixes S :: "'a::{metric_space, second_countable_topology} set"
   obtains T where "countable T" "T \<subseteq> S" "S \<subseteq> closure T"
 proof -
   obtain \<B> :: "'a set set"
     where "countable \<B>"
       and "{} \<notin> \<B>"
       and ope: "\<And>C. C \<in> \<B> \<Longrightarrow> openin(top_of_set S) C"
       and if_ope: "\<And>T. openin(top_of_set S) T \<Longrightarrow> \<exists>\<U>. \<U> \<subseteq> \<B> \<and> T = \<Union>\<U>"
     by (meson subset_second_countable)
   then obtain f where f: "\<And>C. C \<in> \<B> \<Longrightarrow> f C \<in> C"
     by (metis equals0I)
   show ?thesis
   proof
     show "countable (f ` \<B>)"
       by (simp add: \<open>countable \<B>\<close>)
     show "f ` \<B> \<subseteq> S"
       using ope f openin_imp_subset by blast
     show "S \<subseteq> closure (f ` \<B>)"
     proof (clarsimp simp: closure_approachable)
       fix x and e::real
       assume "x \<in> S" "0 < e"
       have "openin (top_of_set S) (S \<inter> ball x e)"
         by (simp add: openin_Int_open)
       with if_ope obtain \<U> where  \<U>: "\<U> \<subseteq> \<B>" "S \<inter> ball x e = \<Union>\<U>"
         by meson
       show "\<exists>C \<in> \<B>. dist (f C) x < e"
       proof (cases "\<U> = {}")
         case True
         then show ?thesis
           using \<open>0 < e\<close>  \<U> \<open>x \<in> S\<close> by auto
       next
         case False
         then obtain C where "C \<in> \<U>" by blast
         show ?thesis
         proof
           show "dist (f C) x < e"
             by (metis Int_iff Union_iff \<U> \<open>C \<in> \<U>\<close> dist_commute f mem_ball subsetCE)
           show "C \<in> \<B>"
             using \<open>\<U> \<subseteq> \<B>\<close> \<open>C \<in> \<U>\<close> by blast
         qed
       qed
     qed
   qed
 qed
 
 
 subsection\<^marker>\<open>tag unimportant\<close> \<open>Diameter\<close>
 
 lemma diameter_cball [simp]:
   fixes a :: "'a::euclidean_space"
   shows "diameter(cball a r) = (if r < 0 then 0 else 2*r)"
 proof -
   have "diameter(cball a r) = 2*r" if "r \<ge> 0"
   proof (rule order_antisym)
     show "diameter (cball a r) \<le> 2*r"
     proof (rule diameter_le)
       fix x y assume "x \<in> cball a r" "y \<in> cball a r"
       then have "norm (x - a) \<le> r" "norm (a - y) \<le> r"
         by (auto simp: dist_norm norm_minus_commute)
       then have "norm (x - y) \<le> r+r"
         using norm_diff_triangle_le by blast
       then show "norm (x - y) \<le> 2*r" by simp
     qed (simp add: that)
     have "2*r = dist (a + r *\<^sub>R (SOME i. i \<in> Basis)) (a - r *\<^sub>R (SOME i. i \<in> Basis))"
       apply (simp add: dist_norm)
       by (metis abs_of_nonneg mult.right_neutral norm_numeral norm_scaleR norm_some_Basis real_norm_def scaleR_2 that)
     also have "... \<le> diameter (cball a r)"
       apply (rule diameter_bounded_bound)
       using that by (auto simp: dist_norm)
     finally show "2*r \<le> diameter (cball a r)" .
   qed
   then show ?thesis by simp
 qed
 
 lemma diameter_ball [simp]:
   fixes a :: "'a::euclidean_space"
   shows "diameter(ball a r) = (if r < 0 then 0 else 2*r)"
 proof -
   have "diameter(ball a r) = 2*r" if "r > 0"
     by (metis bounded_ball diameter_closure closure_ball diameter_cball less_eq_real_def linorder_not_less that)
   then show ?thesis
     by (simp add: diameter_def)
 qed
 
 lemma diameter_closed_interval [simp]: "diameter {a..b} = (if b < a then 0 else b-a)"
 proof -
   have "{a .. b} = cball ((a+b)/2) ((b-a)/2)"
     by (auto simp: dist_norm abs_if field_split_simps split: if_split_asm)
   then show ?thesis
     by simp
 qed
 
 lemma diameter_open_interval [simp]: "diameter {a<..<b} = (if b < a then 0 else b-a)"
 proof -
   have "{a <..< b} = ball ((a+b)/2) ((b-a)/2)"
     by (auto simp: dist_norm abs_if field_split_simps split: if_split_asm)
   then show ?thesis
     by simp
 qed
 
 lemma diameter_cbox:
   fixes a b::"'a::euclidean_space"
   shows "(\<forall>i \<in> Basis. a \<bullet> i \<le> b \<bullet> i) \<Longrightarrow> diameter (cbox a b) = dist a b"
   by (force simp: diameter_def intro!: cSup_eq_maximum L2_set_mono
      simp: euclidean_dist_l2[where 'a='a] cbox_def dist_norm)
 
 
 subsection\<^marker>\<open>tag unimportant\<close>\<open>Relating linear images to open/closed/interior/closure/connected\<close>
 
 proposition open_surjective_linear_image:
   fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::euclidean_space"
   assumes "open A" "linear f" "surj f"
     shows "open(f ` A)"
 unfolding open_dist
 proof clarify
   fix x
   assume "x \<in> A"
   have "bounded (inv f ` Basis)"
     by (simp add: finite_imp_bounded)
   with bounded_pos obtain B where "B > 0" and B: "\<And>x. x \<in> inv f ` Basis \<Longrightarrow> norm x \<le> B"
     by metis
   obtain e where "e > 0" and e: "\<And>z. dist z x < e \<Longrightarrow> z \<in> A"
     by (metis open_dist \<open>x \<in> A\<close> \<open>open A\<close>)
   define \<delta> where "\<delta> \<equiv> e / B / DIM('b)"
   show "\<exists>e>0. \<forall>y. dist y (f x) < e \<longrightarrow> y \<in> f ` A"
   proof (intro exI conjI)
     show "\<delta> > 0"
       using \<open>e > 0\<close> \<open>B > 0\<close>  by (simp add: \<delta>_def field_split_simps)
     have "y \<in> f ` A" if "dist y (f x) * (B * real DIM('b)) < e" for y
     proof -
       define u where "u \<equiv> y - f x"
       show ?thesis
       proof (rule image_eqI)
         show "y = f (x + (\<Sum>i\<in>Basis. (u \<bullet> i) *\<^sub>R inv f i))"
           apply (simp add: linear_add linear_sum linear.scaleR \<open>linear f\<close> surj_f_inv_f \<open>surj f\<close>)
           apply (simp add: euclidean_representation u_def)
           done
         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))"
           by (simp add: dist_norm sum_norm_le)
         also have "... = (\<Sum>i\<in>Basis. \<bar>u \<bullet> i\<bar> * norm (inv f i))"
           by simp
         also have "... \<le> (\<Sum>i\<in>Basis. \<bar>u \<bullet> i\<bar>) * B"
           by (simp add: B sum_distrib_right sum_mono mult_left_mono)
         also have "... \<le> DIM('b) * dist y (f x) * B"
           apply (rule mult_right_mono [OF sum_bounded_above])
           using \<open>0 < B\<close> by (auto simp: Basis_le_norm dist_norm u_def)
         also have "... < e"
           by (metis mult.commute mult.left_commute that)
         finally show "x + (\<Sum>i\<in>Basis. (u \<bullet> i) *\<^sub>R inv f i) \<in> A"
           by (rule e)
       qed
     qed
     then show "\<forall>y. dist y (f x) < \<delta> \<longrightarrow> y \<in> f ` A"
       using \<open>e > 0\<close> \<open>B > 0\<close>
       by (auto simp: \<delta>_def field_split_simps)
   qed
 qed
 
 corollary open_bijective_linear_image_eq:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes "linear f" "bij f"
     shows "open(f ` A) \<longleftrightarrow> open A"
 proof
   assume "open(f ` A)"
   then have "open(f -` (f ` A))"
     using assms by (force simp: linear_continuous_at linear_conv_bounded_linear continuous_open_vimage)
   then show "open A"
     by (simp add: assms bij_is_inj inj_vimage_image_eq)
 next
   assume "open A"
   then show "open(f ` A)"
     by (simp add: assms bij_is_surj open_surjective_linear_image)
 qed
 
 corollary interior_bijective_linear_image:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes "linear f" "bij f"
   shows "interior (f ` S) = f ` interior S"  (is "?lhs = ?rhs")
 proof safe
   fix x
   assume x: "x \<in> ?lhs"
   then obtain T where "open T" and "x \<in> T" and "T \<subseteq> f ` S"
     by (metis interiorE)
   then show "x \<in> ?rhs"
     by (metis (no_types, hide_lams) assms subsetD interior_maximal open_bijective_linear_image_eq subset_image_iff)
 next
   fix x
   assume x: "x \<in> interior S"
   then show "f x \<in> interior (f ` S)"
     by (meson assms imageI image_mono interiorI interior_subset open_bijective_linear_image_eq open_interior)
 qed
 
 lemma interior_injective_linear_image:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space"
   assumes "linear f" "inj f"
    shows "interior(f ` S) = f ` (interior S)"
   by (simp add: linear_injective_imp_surjective assms bijI interior_bijective_linear_image)
 
 lemma interior_surjective_linear_image:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space"
   assumes "linear f" "surj f"
    shows "interior(f ` S) = f ` (interior S)"
   by (simp add: assms interior_injective_linear_image linear_surjective_imp_injective)
 
 lemma interior_negations:
   fixes S :: "'a::euclidean_space set"
   shows "interior(uminus ` S) = image uminus (interior S)"
   by (simp add: bij_uminus interior_bijective_linear_image linear_uminus)
 
 lemma connected_linear_image:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
   assumes "linear f" and "connected s"
   shows "connected (f ` s)"
 using connected_continuous_image assms linear_continuous_on linear_conv_bounded_linear by blast
 
 
 subsection\<^marker>\<open>tag unimportant\<close> \<open>"Isometry" (up to constant bounds) of Injective Linear Map\<close>
 
 proposition injective_imp_isometric:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes s: "closed s" "subspace s"
     and f: "bounded_linear f" "\<forall>x\<in>s. f x = 0 \<longrightarrow> x = 0"
   shows "\<exists>e>0. \<forall>x\<in>s. norm (f x) \<ge> e * norm x"
 proof (cases "s \<subseteq> {0::'a}")
   case True
   have "norm x \<le> norm (f x)" if "x \<in> s" for x
   proof -
     from True that have "x = 0" by auto
     then show ?thesis by simp
   qed
   then show ?thesis
     by (auto intro!: exI[where x=1])
 next
   case False
   interpret f: bounded_linear f by fact
   from False obtain a where a: "a \<noteq> 0" "a \<in> s"
     by auto
   from False have "s \<noteq> {}"
     by auto
   let ?S = "{f x| x. x \<in> s \<and> norm x = norm a}"
   let ?S' = "{x::'a. x\<in>s \<and> norm x = norm a}"
   let ?S'' = "{x::'a. norm x = norm a}"
 
   have "?S'' = frontier (cball 0 (norm a))"
     by (simp add: sphere_def dist_norm)
   then have "compact ?S''" by (metis compact_cball compact_frontier)
   moreover have "?S' = s \<inter> ?S''" by auto
   ultimately have "compact ?S'"
     using closed_Int_compact[of s ?S''] using s(1) by auto
   moreover have *:"f ` ?S' = ?S" by auto
   ultimately have "compact ?S"
     using compact_continuous_image[OF linear_continuous_on[OF f(1)], of ?S'] by auto
   then have "closed ?S"
     using compact_imp_closed by auto
   moreover from a have "?S \<noteq> {}" by auto
   ultimately obtain b' where "b'\<in>?S" "\<forall>y\<in>?S. norm b' \<le> norm y"
     using distance_attains_inf[of ?S 0] unfolding dist_0_norm by auto
   then obtain b where "b\<in>s"
     and ba: "norm b = norm a"
     and b: "\<forall>x\<in>{x \<in> s. norm x = norm a}. norm (f b) \<le> norm (f x)"
     unfolding *[symmetric] unfolding image_iff by auto
 
   let ?e = "norm (f b) / norm b"
   have "norm b > 0"
     using ba and a and norm_ge_zero by auto
   moreover have "norm (f b) > 0"
     using f(2)[THEN bspec[where x=b], OF \<open>b\<in>s\<close>]
     using \<open>norm b >0\<close> by simp
   ultimately have "0 < norm (f b) / norm b" by simp
   moreover
   have "norm (f b) / norm b * norm x \<le> norm (f x)" if "x\<in>s" for x
   proof (cases "x = 0")
     case True
     then show "norm (f b) / norm b * norm x \<le> norm (f x)"
       by auto
   next
     case False
     with \<open>a \<noteq> 0\<close> have *: "0 < norm a / norm x"
       unfolding zero_less_norm_iff[symmetric] by simp
     have "\<forall>x\<in>s. c *\<^sub>R x \<in> s" for c
       using s[unfolded subspace_def] by simp
     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}"
       by simp
     with \<open>x \<noteq> 0\<close> \<open>a \<noteq> 0\<close> show "norm (f b) / norm b * norm x \<le> norm (f x)"
       using b[THEN bspec[where x="(norm a / norm x) *\<^sub>R x"]]
       unfolding f.scaleR and ba
       by (auto simp: mult.commute pos_le_divide_eq pos_divide_le_eq)
   qed
   ultimately show ?thesis by auto
 qed
 
 proposition closed_injective_image_subspace:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes "subspace s" "bounded_linear f" "\<forall>x\<in>s. f x = 0 \<longrightarrow> x = 0" "closed s"
   shows "closed(f ` s)"
 proof -
   obtain e where "e > 0" and e: "\<forall>x\<in>s. e * norm x \<le> norm (f x)"
     using injective_imp_isometric[OF assms(4,1,2,3)] by auto
   show ?thesis
     using complete_isometric_image[OF \<open>e>0\<close> assms(1,2) e] and assms(4)
     unfolding complete_eq_closed[symmetric] by auto
 qed
+                               
+
+lemma closure_bounded_linear_image_subset:
+  assumes f: "bounded_linear f"
+  shows "f ` closure S \<subseteq> closure (f ` S)"
+  using linear_continuous_on [OF f] closed_closure closure_subset
+  by (rule image_closure_subset)
+
+lemma closure_linear_image_subset:
+  fixes f :: "'m::euclidean_space \<Rightarrow> 'n::real_normed_vector"
+  assumes "linear f"
+  shows "f ` (closure S) \<subseteq> closure (f ` S)"
+  using assms unfolding linear_conv_bounded_linear
+  by (rule closure_bounded_linear_image_subset)
+
+lemma closed_injective_linear_image:
+    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+    assumes S: "closed S" and f: "linear f" "inj f"
+    shows "closed (f ` S)"
+proof -
+  obtain g where g: "linear g" "g \<circ> f = id"
+    using linear_injective_left_inverse [OF f] by blast
+  then have confg: "continuous_on (range f) g"
+    using linear_continuous_on linear_conv_bounded_linear by blast
+  have [simp]: "g ` f ` S = S"
+    using g by (simp add: image_comp)
+  have cgf: "closed (g ` f ` S)"
+    by (simp add: \<open>g \<circ> f = id\<close> S image_comp)
+  have [simp]: "(range f \<inter> g -` S) = f ` S"
+    using g unfolding o_def id_def image_def by auto metis+
+  show ?thesis
+  proof (rule closedin_closed_trans [of "range f"])
+    show "closedin (top_of_set (range f)) (f ` S)"
+      using continuous_closedin_preimage [OF confg cgf] by simp
+    show "closed (range f)"
+      apply (rule closed_injective_image_subspace)
+      using f apply (auto simp: linear_linear linear_injective_0)
+      done
+  qed
+qed
+
+lemma closed_injective_linear_image_eq:
+    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+    assumes f: "linear f" "inj f"
+      shows "(closed(image f s) \<longleftrightarrow> closed s)"
+  by (metis closed_injective_linear_image closure_eq closure_linear_image_subset closure_subset_eq f(1) f(2) inj_image_subset_iff)
+
+lemma closure_injective_linear_image:
+    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+    shows "\<lbrakk>linear f; inj f\<rbrakk> \<Longrightarrow> f ` (closure S) = closure (f ` S)"
+  apply (rule subset_antisym)
+  apply (simp add: closure_linear_image_subset)
+  by (simp add: closure_minimal closed_injective_linear_image closure_subset image_mono)
+
+lemma closure_bounded_linear_image:
+    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+    shows "\<lbrakk>linear f; bounded S\<rbrakk> \<Longrightarrow> f ` (closure S) = closure (f ` S)"
+  apply (rule subset_antisym, simp add: closure_linear_image_subset)
+  apply (rule closure_minimal, simp add: closure_subset image_mono)
+  by (meson bounded_closure closed_closure compact_continuous_image compact_eq_bounded_closed linear_continuous_on linear_conv_bounded_linear)
+
+lemma closure_scaleR:
+  fixes S :: "'a::real_normed_vector set"
+  shows "((*\<^sub>R) c) ` (closure S) = closure (((*\<^sub>R) c) ` S)"
+proof
+  show "((*\<^sub>R) c) ` (closure S) \<subseteq> closure (((*\<^sub>R) c) ` S)"
+    using bounded_linear_scaleR_right
+    by (rule closure_bounded_linear_image_subset)
+  show "closure (((*\<^sub>R) c) ` S) \<subseteq> ((*\<^sub>R) c) ` (closure S)"
+    by (intro closure_minimal image_mono closure_subset closed_scaling closed_closure)
+qed
 
 
 subsection\<^marker>\<open>tag unimportant\<close> \<open>Some properties of a canonical subspace\<close>
 
 lemma closed_substandard: "closed {x::'a::euclidean_space. \<forall>i\<in>Basis. P i \<longrightarrow> x\<bullet>i = 0}"
   (is "closed ?A")
 proof -
   let ?D = "{i\<in>Basis. P i}"
   have "closed (\<Inter>i\<in>?D. {x::'a. x\<bullet>i = 0})"
     by (simp add: closed_INT closed_Collect_eq continuous_on_inner)
   also have "(\<Inter>i\<in>?D. {x::'a. x\<bullet>i = 0}) = ?A"
     by auto
   finally show "closed ?A" .
 qed
 
 lemma closed_subspace:
   fixes s :: "'a::euclidean_space set"
   assumes "subspace s"
   shows "closed s"
 proof -
   have "dim s \<le> card (Basis :: 'a set)"
     using dim_subset_UNIV by auto
   with ex_card[OF this] obtain d :: "'a set" where t: "card d = dim s" and d: "d \<subseteq> Basis"
     by auto
   let ?t = "{x::'a. \<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x\<bullet>i = 0}"
   have "\<exists>f. linear f \<and> f ` {x::'a. \<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x \<bullet> i = 0} = s \<and>
       inj_on f {x::'a. \<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x \<bullet> i = 0}"
     using dim_substandard[of d] t d assms
     by (intro subspace_isomorphism[OF subspace_substandard[of "\<lambda>i. i \<notin> d"]]) (auto simp: inner_Basis)
   then obtain f where f:
       "linear f"
       "f ` {x. \<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x \<bullet> i = 0} = s"
       "inj_on f {x. \<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x \<bullet> i = 0}"
     by blast
   interpret f: bounded_linear f
     using f by (simp add: linear_conv_bounded_linear)
   have "x \<in> ?t \<Longrightarrow> f x = 0 \<Longrightarrow> x = 0" for x
     using f.zero d f(3)[THEN inj_onD, of x 0] by auto
   moreover have "closed ?t" by (rule closed_substandard)
   moreover have "subspace ?t" by (rule subspace_substandard)
   ultimately show ?thesis
     using closed_injective_image_subspace[of ?t f]
     unfolding f(2) using f(1) unfolding linear_conv_bounded_linear by auto
 qed
 
 lemma complete_subspace: "subspace s \<Longrightarrow> complete s"
   for s :: "'a::euclidean_space set"
   using complete_eq_closed closed_subspace by auto
 
 lemma closed_span [iff]: "closed (span s)"
   for s :: "'a::euclidean_space set"
   by (simp add: closed_subspace)
 
 lemma dim_closure [simp]: "dim (closure s) = dim s" (is "?dc = ?d")
   for s :: "'a::euclidean_space set"
 proof -
   have "?dc \<le> ?d"
     using closure_minimal[OF span_superset, of s]
     using closed_subspace[OF subspace_span, of s]
     using dim_subset[of "closure s" "span s"]
     by simp
   then show ?thesis
     using dim_subset[OF closure_subset, of s]
     by simp
 qed
 
 
 subsection \<open>Set Distance\<close>
 
 lemma setdist_compact_closed:
   fixes A :: "'a::heine_borel set"
   assumes A: "compact A" and B: "closed B"
     and "A \<noteq> {}" "B \<noteq> {}"
   shows "\<exists>x \<in> A. \<exists>y \<in> B. dist x y = setdist A B"
 proof -
   obtain x where "x \<in> A" "setdist A B = infdist x B"
     by (metis A assms(3) setdist_attains_inf setdist_sym)
   moreover
   obtain y where"y \<in> B" "infdist x B = dist x y"
     using B \<open>B \<noteq> {}\<close> infdist_attains_inf by blast
   ultimately show ?thesis
     using \<open>x \<in> A\<close> \<open>y \<in> B\<close> by auto
 qed
 
 lemma setdist_closed_compact:
   fixes S :: "'a::heine_borel set"
   assumes S: "closed S" and T: "compact T"
       and "S \<noteq> {}" "T \<noteq> {}"
     shows "\<exists>x \<in> S. \<exists>y \<in> T. dist x y = setdist S T"
   using setdist_compact_closed [OF T S \<open>T \<noteq> {}\<close> \<open>S \<noteq> {}\<close>]
   by (metis dist_commute setdist_sym)
 
 lemma setdist_eq_0_compact_closed:
   assumes S: "compact S" and T: "closed T"
     shows "setdist S T = 0 \<longleftrightarrow> S = {} \<or> T = {} \<or> S \<inter> T \<noteq> {}"
 proof (cases "S = {} \<or> T = {}")
   case True
   then show ?thesis
     by force
 next
   case False
   then show ?thesis
     by (metis S T disjoint_iff_not_equal in_closed_iff_infdist_zero setdist_attains_inf setdist_eq_0I setdist_sym)
 qed
 
 corollary setdist_gt_0_compact_closed:
   assumes S: "compact S" and T: "closed T"
     shows "setdist S T > 0 \<longleftrightarrow> (S \<noteq> {} \<and> T \<noteq> {} \<and> S \<inter> T = {})"
   using setdist_pos_le [of S T] setdist_eq_0_compact_closed [OF assms] by linarith
 
 lemma setdist_eq_0_closed_compact:
   assumes S: "closed S" and T: "compact T"
     shows "setdist S T = 0 \<longleftrightarrow> S = {} \<or> T = {} \<or> S \<inter> T \<noteq> {}"
   using setdist_eq_0_compact_closed [OF T S]
   by (metis Int_commute setdist_sym)
 
 lemma setdist_eq_0_bounded:
   fixes S :: "'a::heine_borel set"
   assumes "bounded S \<or> bounded T"
   shows "setdist S T = 0 \<longleftrightarrow> S = {} \<or> T = {} \<or> closure S \<inter> closure T \<noteq> {}"
 proof (cases "S = {} \<or> T = {}")
   case False
   then show ?thesis
     using setdist_eq_0_compact_closed [of "closure S" "closure T"]
           setdist_eq_0_closed_compact [of "closure S" "closure T"] assms
     by (force simp:  bounded_closure compact_eq_bounded_closed)
 qed force
 
 lemma setdist_eq_0_sing_1:
   "setdist {x} S = 0 \<longleftrightarrow> S = {} \<or> x \<in> closure S"
   by (metis in_closure_iff_infdist_zero infdist_def infdist_eq_setdist)
 
 lemma setdist_eq_0_sing_2:
   "setdist S {x} = 0 \<longleftrightarrow> S = {} \<or> x \<in> closure S"
   by (metis setdist_eq_0_sing_1 setdist_sym)
 
 lemma setdist_neq_0_sing_1:
   "\<lbrakk>setdist {x} S = a; a \<noteq> 0\<rbrakk> \<Longrightarrow> S \<noteq> {} \<and> x \<notin> closure S"
   by (metis setdist_closure_2 setdist_empty2 setdist_eq_0I singletonI)
 
 lemma setdist_neq_0_sing_2:
   "\<lbrakk>setdist S {x} = a; a \<noteq> 0\<rbrakk> \<Longrightarrow> S \<noteq> {} \<and> x \<notin> closure S"
   by (simp add: setdist_neq_0_sing_1 setdist_sym)
 
 lemma setdist_sing_in_set:
    "x \<in> S \<Longrightarrow> setdist {x} S = 0"
   by (simp add: setdist_eq_0I)
 
 lemma setdist_eq_0_closed:
    "closed S \<Longrightarrow> (setdist {x} S = 0 \<longleftrightarrow> S = {} \<or> x \<in> S)"
 by (simp add: setdist_eq_0_sing_1)
 
 lemma setdist_eq_0_closedin:
   shows "\<lbrakk>closedin (top_of_set U) S; x \<in> U\<rbrakk>
          \<Longrightarrow> (setdist {x} S = 0 \<longleftrightarrow> S = {} \<or> x \<in> S)"
   by (auto simp: closedin_limpt setdist_eq_0_sing_1 closure_def)
 
 lemma setdist_gt_0_closedin:
   shows "\<lbrakk>closedin (top_of_set U) S; x \<in> U; S \<noteq> {}; x \<notin> S\<rbrakk>
          \<Longrightarrow> setdist {x} S > 0"
   using less_eq_real_def setdist_eq_0_closedin by fastforce
 
 no_notation
   eucl_less (infix "<e" 50)
 
 end