# HG changeset patch
# User immler
# Date 1566943694 -7200
# Node ID f95193669ad7e0feefd5ea4fc43ea36c666277c5
# Parent  191bb458b95c465380afcd021d218742126c91c6
removed Brouwer_Fixpoint from imports of Derivative

diff -r 191bb458b95c -r f95193669ad7 src/HOL/Analysis/Brouwer_Fixpoint.thy
--- a/src/HOL/Analysis/Brouwer_Fixpoint.thy	Tue Aug 27 23:12:28 2019 +0200
+++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy	Wed Aug 28 00:08:14 2019 +0200
@@ -19,6 +19,7 @@
     Path_Connected
     Homeomorphism
     Continuous_Extension
+    Derivative
 begin
 
 subsection \<open>Retractions\<close>
@@ -4936,4 +4937,249 @@
   shows "connected(-S)"
   using assms path_connected_complement_homeomorphic_interval path_connected_imp_connected by blast
 
+subsubsection \<open>Proving surjectivity via Brouwer fixpoint theorem\<close>
+
+lemma brouwer_surjective:
+  fixes f :: "'n::euclidean_space \<Rightarrow> 'n"
+  assumes "compact T"
+    and "convex T"
+    and "T \<noteq> {}"
+    and "continuous_on T f"
+    and "\<And>x y. \<lbrakk>x\<in>S; y\<in>T\<rbrakk> \<Longrightarrow> x + (y - f y) \<in> T"
+    and "x \<in> S"
+  shows "\<exists>y\<in>T. f y = x"
+proof -
+  have *: "\<And>x y. f y = x \<longleftrightarrow> x + (y - f y) = y"
+    by (auto simp add: algebra_simps)
+  show ?thesis
+    unfolding *
+    apply (rule brouwer[OF assms(1-3), of "\<lambda>y. x + (y - f y)"])
+    apply (intro continuous_intros)
+    using assms
+    apply auto
+    done
+qed
+
+lemma brouwer_surjective_cball:
+  fixes f :: "'n::euclidean_space \<Rightarrow> 'n"
+  assumes "continuous_on (cball a e) f"
+    and "e > 0"
+    and "x \<in> S"
+    and "\<And>x y. \<lbrakk>x\<in>S; y\<in>cball a e\<rbrakk> \<Longrightarrow> x + (y - f y) \<in> cball a e"
+  shows "\<exists>y\<in>cball a e. f y = x"
+  apply (rule brouwer_surjective)
+  apply (rule compact_cball convex_cball)+
+  unfolding cball_eq_empty
+  using assms
+  apply auto
+  done
+
+subsubsection \<open>Inverse function theorem\<close>
+
+text \<open>See Sussmann: "Multidifferential calculus", Theorem 2.1.1\<close>
+
+lemma sussmann_open_mapping:
+  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::euclidean_space"
+  assumes "open S"
+    and contf: "continuous_on S f"
+    and "x \<in> S"
+    and derf: "(f has_derivative f') (at x)"
+    and "bounded_linear g'" "f' \<circ> g' = id"
+    and "T \<subseteq> S"
+    and x: "x \<in> interior T"
+  shows "f x \<in> interior (f ` T)"
+proof -
+  interpret f': bounded_linear f'
+    using assms unfolding has_derivative_def by auto
+  interpret g': bounded_linear g'
+    using assms by auto
+  obtain B where B: "0 < B" "\<forall>x. norm (g' x) \<le> norm x * B"
+    using bounded_linear.pos_bounded[OF assms(5)] by blast
+  hence *: "1 / (2 * B) > 0" by auto
+  obtain e0 where e0:
+      "0 < e0"
+      "\<forall>y. norm (y - x) < e0 \<longrightarrow> norm (f y - f x - f' (y - x)) \<le> 1 / (2 * B) * norm (y - x)"
+    using derf unfolding has_derivative_at_alt
+    using * by blast
+  obtain e1 where e1: "0 < e1" "cball x e1 \<subseteq> T"
+    using mem_interior_cball x by blast
+  have *: "0 < e0 / B" "0 < e1 / B" using e0 e1 B by auto
+  obtain e where e: "0 < e" "e < e0 / B" "e < e1 / B"
+    using field_lbound_gt_zero[OF *] by blast
+  have lem: "\<exists>y\<in>cball (f x) e. f (x + g' (y - f x)) = z" if "z\<in>cball (f x) (e / 2)" for z
+  proof (rule brouwer_surjective_cball)
+    have z: "z \<in> S" if as: "y \<in>cball (f x) e" "z = x + (g' y - g' (f x))" for y z
+    proof-
+      have "dist x z = norm (g' (f x) - g' y)"
+        unfolding as(2) and dist_norm by auto
+      also have "\<dots> \<le> norm (f x - y) * B"
+        by (metis B(2) g'.diff)
+      also have "\<dots> \<le> e * B"
+        by (metis B(1) dist_norm mem_cball real_mult_le_cancel_iff1 that(1))
+      also have "\<dots> \<le> e1"
+        using B(1) e(3) pos_less_divide_eq by fastforce
+      finally have "z \<in> cball x e1"
+        by force
+      then show "z \<in> S"
+        using e1 assms(7) by auto
+    qed
+    show "continuous_on (cball (f x) e) (\<lambda>y. f (x + g' (y - f x)))"
+      unfolding g'.diff
+    proof (rule continuous_on_compose2 [OF _ _ order_refl, of _ _ f])
+      show "continuous_on ((\<lambda>y. x + (g' y - g' (f x))) ` cball (f x) e) f"
+        by (rule continuous_on_subset[OF contf]) (use z in blast)
+      show "continuous_on (cball (f x) e) (\<lambda>y. x + (g' y - g' (f x)))"
+        by (intro continuous_intros linear_continuous_on[OF \<open>bounded_linear g'\<close>])
+    qed
+  next
+    fix y z
+    assume y: "y \<in> cball (f x) (e / 2)" and z: "z \<in> cball (f x) e"
+    have "norm (g' (z - f x)) \<le> norm (z - f x) * B"
+      using B by auto
+    also have "\<dots> \<le> e * B"
+      by (metis B(1) z dist_norm mem_cball norm_minus_commute real_mult_le_cancel_iff1)
+    also have "\<dots> < e0"
+      using B(1) e(2) pos_less_divide_eq by blast
+    finally have *: "norm (x + g' (z - f x) - x) < e0"
+      by auto
+    have **: "f x + f' (x + g' (z - f x) - x) = z"
+      using assms(6)[unfolded o_def id_def,THEN cong]
+      by auto
+    have "norm (f x - (y + (z - f (x + g' (z - f x))))) \<le>
+          norm (f (x + g' (z - f x)) - z) + norm (f x - y)"
+      using norm_triangle_ineq[of "f (x + g'(z - f x)) - z" "f x - y"]
+      by (auto simp add: algebra_simps)
+    also have "\<dots> \<le> 1 / (B * 2) * norm (g' (z - f x)) + norm (f x - y)"
+      using e0(2)[rule_format, OF *]
+      by (simp only: algebra_simps **) auto
+    also have "\<dots> \<le> 1 / (B * 2) * norm (g' (z - f x)) + e/2"
+      using y by (auto simp: dist_norm)
+    also have "\<dots> \<le> 1 / (B * 2) * B * norm (z - f x) + e/2"
+      using * B by (auto simp add: field_simps)
+    also have "\<dots> \<le> 1 / 2 * norm (z - f x) + e/2"
+      by auto
+    also have "\<dots> \<le> e/2 + e/2"
+      using B(1) \<open>norm (z - f x) * B \<le> e * B\<close> by auto
+    finally show "y + (z - f (x + g' (z - f x))) \<in> cball (f x) e"
+      by (auto simp: dist_norm)
+  qed (use e that in auto) 
+  show ?thesis
+    unfolding mem_interior
+  proof (intro exI conjI subsetI)
+    fix y
+    assume "y \<in> ball (f x) (e / 2)"
+    then have *: "y \<in> cball (f x) (e / 2)"
+      by auto
+    obtain z where z: "z \<in> cball (f x) e" "f (x + g' (z - f x)) = y"
+      using lem * by blast
+    then have "norm (g' (z - f x)) \<le> norm (z - f x) * B"
+      using B
+      by (auto simp add: field_simps)
+    also have "\<dots> \<le> e * B"
+      by (metis B(1) dist_norm mem_cball norm_minus_commute real_mult_le_cancel_iff1 z(1))
+    also have "\<dots> \<le> e1"
+      using e B unfolding less_divide_eq by auto
+    finally have "x + g'(z - f x) \<in> T"
+      by (metis add_diff_cancel diff_diff_add dist_norm e1(2) mem_cball norm_minus_commute subset_eq)
+    then show "y \<in> f ` T"
+      using z by auto
+  qed (use e in auto)
+qed
+
+text \<open>Hence the following eccentric variant of the inverse function theorem.
+  This has no continuity assumptions, but we do need the inverse function.
+  We could put \<open>f' \<circ> g = I\<close> but this happens to fit with the minimal linear
+  algebra theory I've set up so far.\<close>
+
+lemma has_derivative_inverse_strong:
+  fixes f :: "'n::euclidean_space \<Rightarrow> 'n"
+  assumes "open S"
+    and "x \<in> S"
+    and contf: "continuous_on S f"
+    and gf: "\<And>x. x \<in> S \<Longrightarrow> g (f x) = x"
+    and derf: "(f has_derivative f') (at x)"
+    and id: "f' \<circ> g' = id"
+  shows "(g has_derivative g') (at (f x))"
+proof -
+  have linf: "bounded_linear f'"
+    using derf unfolding has_derivative_def by auto
+  then have ling: "bounded_linear g'"
+    unfolding linear_conv_bounded_linear[symmetric]
+    using id right_inverse_linear by blast
+  moreover have "g' \<circ> f' = id"
+    using id linf ling
+    unfolding linear_conv_bounded_linear[symmetric]
+    using linear_inverse_left
+    by auto
+  moreover have *: "\<And>T. \<lbrakk>T \<subseteq> S; x \<in> interior T\<rbrakk> \<Longrightarrow> f x \<in> interior (f ` T)"
+    apply (rule sussmann_open_mapping)
+    apply (rule assms ling)+
+    apply auto
+    done
+  have "continuous (at (f x)) g"
+    unfolding continuous_at Lim_at
+  proof (rule, rule)
+    fix e :: real
+    assume "e > 0"
+    then have "f x \<in> interior (f ` (ball x e \<inter> S))"
+      using *[rule_format,of "ball x e \<inter> S"] \<open>x \<in> S\<close>
+      by (auto simp add: interior_open[OF open_ball] interior_open[OF assms(1)])
+    then obtain d where d: "0 < d" "ball (f x) d \<subseteq> f ` (ball x e \<inter> S)"
+      unfolding mem_interior by blast
+    show "\<exists>d>0. \<forall>y. 0 < dist y (f x) \<and> dist y (f x) < d \<longrightarrow> dist (g y) (g (f x)) < e"
+    proof (intro exI allI impI conjI)
+      fix y
+      assume "0 < dist y (f x) \<and> dist y (f x) < d"
+      then have "g y \<in> g ` f ` (ball x e \<inter> S)"
+        by (metis d(2) dist_commute mem_ball rev_image_eqI subset_iff)
+      then show "dist (g y) (g (f x)) < e"
+        using gf[OF \<open>x \<in> S\<close>]
+        by (simp add: assms(4) dist_commute image_iff)
+    qed (use d in auto)
+  qed
+  moreover have "f x \<in> interior (f ` S)"
+    apply (rule sussmann_open_mapping)
+    apply (rule assms ling)+
+    using interior_open[OF assms(1)] and \<open>x \<in> S\<close>
+    apply auto
+    done
+  moreover have "f (g y) = y" if "y \<in> interior (f ` S)" for y
+    by (metis gf imageE interiorE subsetD that)
+  ultimately show ?thesis using assms
+    by (metis has_derivative_inverse_basic_x open_interior)
+qed
+
+text \<open>A rewrite based on the other domain.\<close>
+
+lemma has_derivative_inverse_strong_x:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'a"
+  assumes "open S"
+    and "g y \<in> S"
+    and "continuous_on S f"
+    and "\<And>x. x \<in> S \<Longrightarrow> g (f x) = x"
+    and "(f has_derivative f') (at (g y))"
+    and "f' \<circ> g' = id"
+    and "f (g y) = y"
+  shows "(g has_derivative g') (at y)"
+  using has_derivative_inverse_strong[OF assms(1-6)]
+  unfolding assms(7)
+  by simp
+
+text \<open>On a region.\<close>
+
+theorem has_derivative_inverse_on:
+  fixes f :: "'n::euclidean_space \<Rightarrow> 'n"
+  assumes "open S"
+    and derf: "\<And>x. x \<in> S \<Longrightarrow> (f has_derivative f'(x)) (at x)"
+    and "\<And>x. x \<in> S \<Longrightarrow> g (f x) = x"
+    and "f' x \<circ> g' x = id"
+    and "x \<in> S"
+  shows "(g has_derivative g'(x)) (at (f x))"
+proof (rule has_derivative_inverse_strong[where g'="g' x" and f=f])
+  show "continuous_on S f"
+  unfolding continuous_on_eq_continuous_at[OF \<open>open S\<close>]
+  using derf has_derivative_continuous by blast
+qed (use assms in auto)
+
+
 end
diff -r 191bb458b95c -r f95193669ad7 src/HOL/Analysis/Complex_Analysis_Basics.thy
--- a/src/HOL/Analysis/Complex_Analysis_Basics.thy	Tue Aug 27 23:12:28 2019 +0200
+++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy	Wed Aug 28 00:08:14 2019 +0200
@@ -5,7 +5,7 @@
 section \<open>Complex Analysis Basics\<close>
 
 theory Complex_Analysis_Basics
-  imports Derivative "HOL-Library.Nonpos_Ints"
+  imports Brouwer_Fixpoint "HOL-Library.Nonpos_Ints"
 begin
 
 (* TODO FIXME: A lot of the things in here have nothing to do with complex analysis *)
diff -r 191bb458b95c -r f95193669ad7 src/HOL/Analysis/Derivative.thy
--- a/src/HOL/Analysis/Derivative.thy	Tue Aug 27 23:12:28 2019 +0200
+++ b/src/HOL/Analysis/Derivative.thy	Wed Aug 28 00:08:14 2019 +0200
@@ -6,7 +6,11 @@
 section \<open>Derivative\<close>
 
 theory Derivative
-imports Brouwer_Fixpoint Operator_Norm Uniform_Limit Bounded_Linear_Function
+  imports
+    Path_Connected
+    Operator_Norm
+    Uniform_Limit
+    Bounded_Linear_Function
 begin
 
 declare bounded_linear_inner_left [intro]
@@ -1203,251 +1207,6 @@
 qed
 
 
-subsection \<open>Inverse function theorem\<close>
-
-text \<open>Proving surjectivity via Brouwer fixpoint theorem\<close>
-
-lemma brouwer_surjective:
-  fixes f :: "'n::euclidean_space \<Rightarrow> 'n"
-  assumes "compact T"
-    and "convex T"
-    and "T \<noteq> {}"
-    and "continuous_on T f"
-    and "\<And>x y. \<lbrakk>x\<in>S; y\<in>T\<rbrakk> \<Longrightarrow> x + (y - f y) \<in> T"
-    and "x \<in> S"
-  shows "\<exists>y\<in>T. f y = x"
-proof -
-  have *: "\<And>x y. f y = x \<longleftrightarrow> x + (y - f y) = y"
-    by (auto simp add: algebra_simps)
-  show ?thesis
-    unfolding *
-    apply (rule brouwer[OF assms(1-3), of "\<lambda>y. x + (y - f y)"])
-    apply (intro continuous_intros)
-    using assms
-    apply auto
-    done
-qed
-
-lemma brouwer_surjective_cball:
-  fixes f :: "'n::euclidean_space \<Rightarrow> 'n"
-  assumes "continuous_on (cball a e) f"
-    and "e > 0"
-    and "x \<in> S"
-    and "\<And>x y. \<lbrakk>x\<in>S; y\<in>cball a e\<rbrakk> \<Longrightarrow> x + (y - f y) \<in> cball a e"
-  shows "\<exists>y\<in>cball a e. f y = x"
-  apply (rule brouwer_surjective)
-  apply (rule compact_cball convex_cball)+
-  unfolding cball_eq_empty
-  using assms
-  apply auto
-  done
-
-text \<open>See Sussmann: "Multidifferential calculus", Theorem 2.1.1\<close>
-
-lemma sussmann_open_mapping:
-  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::euclidean_space"
-  assumes "open S"
-    and contf: "continuous_on S f"
-    and "x \<in> S"
-    and derf: "(f has_derivative f') (at x)"
-    and "bounded_linear g'" "f' \<circ> g' = id"
-    and "T \<subseteq> S"
-    and x: "x \<in> interior T"
-  shows "f x \<in> interior (f ` T)"
-proof -
-  interpret f': bounded_linear f'
-    using assms unfolding has_derivative_def by auto
-  interpret g': bounded_linear g'
-    using assms by auto
-  obtain B where B: "0 < B" "\<forall>x. norm (g' x) \<le> norm x * B"
-    using bounded_linear.pos_bounded[OF assms(5)] by blast
-  hence *: "1 / (2 * B) > 0" by auto
-  obtain e0 where e0:
-      "0 < e0"
-      "\<forall>y. norm (y - x) < e0 \<longrightarrow> norm (f y - f x - f' (y - x)) \<le> 1 / (2 * B) * norm (y - x)"
-    using derf unfolding has_derivative_at_alt
-    using * by blast
-  obtain e1 where e1: "0 < e1" "cball x e1 \<subseteq> T"
-    using mem_interior_cball x by blast
-  have *: "0 < e0 / B" "0 < e1 / B" using e0 e1 B by auto
-  obtain e where e: "0 < e" "e < e0 / B" "e < e1 / B"
-    using field_lbound_gt_zero[OF *] by blast
-  have lem: "\<exists>y\<in>cball (f x) e. f (x + g' (y - f x)) = z" if "z\<in>cball (f x) (e / 2)" for z
-  proof (rule brouwer_surjective_cball)
-    have z: "z \<in> S" if as: "y \<in>cball (f x) e" "z = x + (g' y - g' (f x))" for y z
-    proof-
-      have "dist x z = norm (g' (f x) - g' y)"
-        unfolding as(2) and dist_norm by auto
-      also have "\<dots> \<le> norm (f x - y) * B"
-        by (metis B(2) g'.diff)
-      also have "\<dots> \<le> e * B"
-        by (metis B(1) dist_norm mem_cball real_mult_le_cancel_iff1 that(1))
-      also have "\<dots> \<le> e1"
-        using B(1) e(3) pos_less_divide_eq by fastforce
-      finally have "z \<in> cball x e1"
-        by force
-      then show "z \<in> S"
-        using e1 assms(7) by auto
-    qed
-    show "continuous_on (cball (f x) e) (\<lambda>y. f (x + g' (y - f x)))"
-      unfolding g'.diff
-    proof (rule continuous_on_compose2 [OF _ _ order_refl, of _ _ f])
-      show "continuous_on ((\<lambda>y. x + (g' y - g' (f x))) ` cball (f x) e) f"
-        by (rule continuous_on_subset[OF contf]) (use z in blast)
-      show "continuous_on (cball (f x) e) (\<lambda>y. x + (g' y - g' (f x)))"
-        by (intro continuous_intros linear_continuous_on[OF \<open>bounded_linear g'\<close>])
-    qed
-  next
-    fix y z
-    assume y: "y \<in> cball (f x) (e / 2)" and z: "z \<in> cball (f x) e"
-    have "norm (g' (z - f x)) \<le> norm (z - f x) * B"
-      using B by auto
-    also have "\<dots> \<le> e * B"
-      by (metis B(1) z dist_norm mem_cball norm_minus_commute real_mult_le_cancel_iff1)
-    also have "\<dots> < e0"
-      using B(1) e(2) pos_less_divide_eq by blast
-    finally have *: "norm (x + g' (z - f x) - x) < e0"
-      by auto
-    have **: "f x + f' (x + g' (z - f x) - x) = z"
-      using assms(6)[unfolded o_def id_def,THEN cong]
-      by auto
-    have "norm (f x - (y + (z - f (x + g' (z - f x))))) \<le>
-          norm (f (x + g' (z - f x)) - z) + norm (f x - y)"
-      using norm_triangle_ineq[of "f (x + g'(z - f x)) - z" "f x - y"]
-      by (auto simp add: algebra_simps)
-    also have "\<dots> \<le> 1 / (B * 2) * norm (g' (z - f x)) + norm (f x - y)"
-      using e0(2)[rule_format, OF *]
-      by (simp only: algebra_simps **) auto
-    also have "\<dots> \<le> 1 / (B * 2) * norm (g' (z - f x)) + e/2"
-      using y by (auto simp: dist_norm)
-    also have "\<dots> \<le> 1 / (B * 2) * B * norm (z - f x) + e/2"
-      using * B by (auto simp add: field_simps)
-    also have "\<dots> \<le> 1 / 2 * norm (z - f x) + e/2"
-      by auto
-    also have "\<dots> \<le> e/2 + e/2"
-      using B(1) \<open>norm (z - f x) * B \<le> e * B\<close> by auto
-    finally show "y + (z - f (x + g' (z - f x))) \<in> cball (f x) e"
-      by (auto simp: dist_norm)
-  qed (use e that in auto) 
-  show ?thesis
-    unfolding mem_interior
-  proof (intro exI conjI subsetI)
-    fix y
-    assume "y \<in> ball (f x) (e / 2)"
-    then have *: "y \<in> cball (f x) (e / 2)"
-      by auto
-    obtain z where z: "z \<in> cball (f x) e" "f (x + g' (z - f x)) = y"
-      using lem * by blast
-    then have "norm (g' (z - f x)) \<le> norm (z - f x) * B"
-      using B
-      by (auto simp add: field_simps)
-    also have "\<dots> \<le> e * B"
-      by (metis B(1) dist_norm mem_cball norm_minus_commute real_mult_le_cancel_iff1 z(1))
-    also have "\<dots> \<le> e1"
-      using e B unfolding less_divide_eq by auto
-    finally have "x + g'(z - f x) \<in> T"
-      by (metis add_diff_cancel diff_diff_add dist_norm e1(2) mem_cball norm_minus_commute subset_eq)
-    then show "y \<in> f ` T"
-      using z by auto
-  qed (use e in auto)
-qed
-
-text \<open>Hence the following eccentric variant of the inverse function theorem.
-  This has no continuity assumptions, but we do need the inverse function.
-  We could put \<open>f' \<circ> g = I\<close> but this happens to fit with the minimal linear
-  algebra theory I've set up so far.\<close>
-
-lemma has_derivative_inverse_strong:
-  fixes f :: "'n::euclidean_space \<Rightarrow> 'n"
-  assumes "open S"
-    and "x \<in> S"
-    and contf: "continuous_on S f"
-    and gf: "\<And>x. x \<in> S \<Longrightarrow> g (f x) = x"
-    and derf: "(f has_derivative f') (at x)"
-    and id: "f' \<circ> g' = id"
-  shows "(g has_derivative g') (at (f x))"
-proof -
-  have linf: "bounded_linear f'"
-    using derf unfolding has_derivative_def by auto
-  then have ling: "bounded_linear g'"
-    unfolding linear_conv_bounded_linear[symmetric]
-    using id right_inverse_linear by blast
-  moreover have "g' \<circ> f' = id"
-    using id linf ling
-    unfolding linear_conv_bounded_linear[symmetric]
-    using linear_inverse_left
-    by auto
-  moreover have *: "\<And>T. \<lbrakk>T \<subseteq> S; x \<in> interior T\<rbrakk> \<Longrightarrow> f x \<in> interior (f ` T)"
-    apply (rule sussmann_open_mapping)
-    apply (rule assms ling)+
-    apply auto
-    done
-  have "continuous (at (f x)) g"
-    unfolding continuous_at Lim_at
-  proof (rule, rule)
-    fix e :: real
-    assume "e > 0"
-    then have "f x \<in> interior (f ` (ball x e \<inter> S))"
-      using *[rule_format,of "ball x e \<inter> S"] \<open>x \<in> S\<close>
-      by (auto simp add: interior_open[OF open_ball] interior_open[OF assms(1)])
-    then obtain d where d: "0 < d" "ball (f x) d \<subseteq> f ` (ball x e \<inter> S)"
-      unfolding mem_interior by blast
-    show "\<exists>d>0. \<forall>y. 0 < dist y (f x) \<and> dist y (f x) < d \<longrightarrow> dist (g y) (g (f x)) < e"
-    proof (intro exI allI impI conjI)
-      fix y
-      assume "0 < dist y (f x) \<and> dist y (f x) < d"
-      then have "g y \<in> g ` f ` (ball x e \<inter> S)"
-        by (metis d(2) dist_commute mem_ball rev_image_eqI subset_iff)
-      then show "dist (g y) (g (f x)) < e"
-        using gf[OF \<open>x \<in> S\<close>]
-        by (simp add: assms(4) dist_commute image_iff)
-    qed (use d in auto)
-  qed
-  moreover have "f x \<in> interior (f ` S)"
-    apply (rule sussmann_open_mapping)
-    apply (rule assms ling)+
-    using interior_open[OF assms(1)] and \<open>x \<in> S\<close>
-    apply auto
-    done
-  moreover have "f (g y) = y" if "y \<in> interior (f ` S)" for y
-    by (metis gf imageE interiorE subsetD that)
-  ultimately show ?thesis using assms
-    by (metis has_derivative_inverse_basic_x open_interior)
-qed
-
-text \<open>A rewrite based on the other domain.\<close>
-
-lemma has_derivative_inverse_strong_x:
-  fixes f :: "'a::euclidean_space \<Rightarrow> 'a"
-  assumes "open S"
-    and "g y \<in> S"
-    and "continuous_on S f"
-    and "\<And>x. x \<in> S \<Longrightarrow> g (f x) = x"
-    and "(f has_derivative f') (at (g y))"
-    and "f' \<circ> g' = id"
-    and "f (g y) = y"
-  shows "(g has_derivative g') (at y)"
-  using has_derivative_inverse_strong[OF assms(1-6)]
-  unfolding assms(7)
-  by simp
-
-text \<open>On a region.\<close>
-
-theorem has_derivative_inverse_on:
-  fixes f :: "'n::euclidean_space \<Rightarrow> 'n"
-  assumes "open S"
-    and derf: "\<And>x. x \<in> S \<Longrightarrow> (f has_derivative f'(x)) (at x)"
-    and "\<And>x. x \<in> S \<Longrightarrow> g (f x) = x"
-    and "f' x \<circ> g' x = id"
-    and "x \<in> S"
-  shows "(g has_derivative g'(x)) (at (f x))"
-proof (rule has_derivative_inverse_strong[where g'="g' x" and f=f])
-  show "continuous_on S f"
-  unfolding continuous_on_eq_continuous_at[OF \<open>open S\<close>]
-  using derf has_derivative_continuous by blast
-qed (use assms in auto)
-
-
 text \<open>Invertible derivative continuous at a point implies local
 injectivity. It's only for this we need continuity of the derivative,
 except of course if we want the fact that the inverse derivative is
diff -r 191bb458b95c -r f95193669ad7 src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Tue Aug 27 23:12:28 2019 +0200
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Wed Aug 28 00:08:14 2019 +0200
@@ -5,7 +5,7 @@
 *)
 
 theory Equivalence_Lebesgue_Henstock_Integration
-  imports Lebesgue_Measure Henstock_Kurzweil_Integration Complete_Measure Set_Integral
+  imports Lebesgue_Measure Henstock_Kurzweil_Integration Complete_Measure Set_Integral Homeomorphism
 begin
 
 lemma le_left_mono: "x \<le> y \<Longrightarrow> y \<le> a \<longrightarrow> x \<le> (a::'a::preorder)"
diff -r 191bb458b95c -r f95193669ad7 src/HOL/Analysis/Further_Topology.thy
--- a/src/HOL/Analysis/Further_Topology.thy	Tue Aug 27 23:12:28 2019 +0200
+++ b/src/HOL/Analysis/Further_Topology.thy	Wed Aug 28 00:08:14 2019 +0200
@@ -6,6 +6,18 @@
   imports Weierstrass_Theorems Polytope Complex_Transcendental Equivalence_Lebesgue_Henstock_Integration
 begin
 
+subsection\<^marker>\<open>tag unimportant\<close>\<open>Retracts and intervals in ordered euclidean space\<close>
+
+lemma ANR_interval [iff]:
+  fixes a :: "'a::ordered_euclidean_space"
+  shows "ANR{a..b}"
+  by (simp add: interval_cbox)
+
+lemma ENR_interval [iff]:
+  fixes a :: "'a::ordered_euclidean_space"
+  shows "ENR{a..b}"
+  by (auto simp: interval_cbox)
+
 subsection\<open>A map from a sphere to a higher dimensional sphere is nullhomotopic\<close>
 
 lemma spheremap_lemma1:
diff -r 191bb458b95c -r f95193669ad7 src/HOL/Analysis/Homeomorphism.thy
--- a/src/HOL/Analysis/Homeomorphism.thy	Tue Aug 27 23:12:28 2019 +0200
+++ b/src/HOL/Analysis/Homeomorphism.thy	Wed Aug 28 00:08:14 2019 +0200
@@ -38,246 +38,6 @@
 
 subsection \<open>Homeomorphism of all convex compact sets with nonempty interior\<close>
 
-proposition ray_to_rel_frontier:
-  fixes a :: "'a::real_inner"
-  assumes "bounded S"
-      and a: "a \<in> rel_interior S"
-      and aff: "(a + l) \<in> affine hull S"
-      and "l \<noteq> 0"
-  obtains d where "0 < d" "(a + d *\<^sub>R l) \<in> rel_frontier S"
-           "\<And>e. \<lbrakk>0 \<le> e; e < d\<rbrakk> \<Longrightarrow> (a + e *\<^sub>R l) \<in> rel_interior S"
-proof -
-  have aaff: "a \<in> affine hull S"
-    by (meson a hull_subset rel_interior_subset rev_subsetD)
-  let ?D = "{d. 0 < d \<and> a + d *\<^sub>R l \<notin> rel_interior S}"
-  obtain B where "B > 0" and B: "S \<subseteq> ball a B"
-    using bounded_subset_ballD [OF \<open>bounded S\<close>] by blast
-  have "a + (B / norm l) *\<^sub>R l \<notin> ball a B"
-    by (simp add: dist_norm \<open>l \<noteq> 0\<close>)
-  with B have "a + (B / norm l) *\<^sub>R l \<notin> rel_interior S"
-    using rel_interior_subset subsetCE by blast
-  with \<open>B > 0\<close> \<open>l \<noteq> 0\<close> have nonMT: "?D \<noteq> {}"
-    using divide_pos_pos zero_less_norm_iff by fastforce
-  have bdd: "bdd_below ?D"
-    by (metis (no_types, lifting) bdd_belowI le_less mem_Collect_eq)
-  have relin_Ex: "\<And>x. x \<in> rel_interior S \<Longrightarrow>
-                    \<exists>e>0. \<forall>x'\<in>affine hull S. dist x' x < e \<longrightarrow> x' \<in> rel_interior S"
-    using openin_rel_interior [of S] by (simp add: openin_euclidean_subtopology_iff)
-  define d where "d = Inf ?D"
-  obtain \<epsilon> where "0 < \<epsilon>" and \<epsilon>: "\<And>\<eta>. \<lbrakk>0 \<le> \<eta>; \<eta> < \<epsilon>\<rbrakk> \<Longrightarrow> (a + \<eta> *\<^sub>R l) \<in> rel_interior S"
-  proof -
-    obtain e where "e>0"
-            and e: "\<And>x'. x' \<in> affine hull S \<Longrightarrow> dist x' a < e \<Longrightarrow> x' \<in> rel_interior S"
-      using relin_Ex a by blast
-    show thesis
-    proof (rule_tac \<epsilon> = "e / norm l" in that)
-      show "0 < e / norm l" by (simp add: \<open>0 < e\<close> \<open>l \<noteq> 0\<close>)
-    next
-      show "a + \<eta> *\<^sub>R l \<in> rel_interior S" if "0 \<le> \<eta>" "\<eta> < e / norm l" for \<eta>
-      proof (rule e)
-        show "a + \<eta> *\<^sub>R l \<in> affine hull S"
-          by (metis (no_types) add_diff_cancel_left' aff affine_affine_hull mem_affine_3_minus aaff)
-        show "dist (a + \<eta> *\<^sub>R l) a < e"
-          using that by (simp add: \<open>l \<noteq> 0\<close> dist_norm pos_less_divide_eq)
-      qed
-    qed
-  qed
-  have inint: "\<And>e. \<lbrakk>0 \<le> e; e < d\<rbrakk> \<Longrightarrow> a + e *\<^sub>R l \<in> rel_interior S"
-    unfolding d_def using cInf_lower [OF _ bdd]
-    by (metis (no_types, lifting) a add.right_neutral le_less mem_Collect_eq not_less real_vector.scale_zero_left)
-  have "\<epsilon> \<le> d"
-    unfolding d_def
-    apply (rule cInf_greatest [OF nonMT])
-    using \<epsilon> dual_order.strict_implies_order le_less_linear by blast
-  with \<open>0 < \<epsilon>\<close> have "0 < d" by simp
-  have "a + d *\<^sub>R l \<notin> rel_interior S"
-  proof
-    assume adl: "a + d *\<^sub>R l \<in> rel_interior S"
-    obtain e where "e > 0"
-             and e: "\<And>x'. x' \<in> affine hull S \<Longrightarrow> dist x' (a + d *\<^sub>R l) < e \<Longrightarrow> x' \<in> rel_interior S"
-      using relin_Ex adl by blast
-    have "d + e / norm l \<le> Inf {d. 0 < d \<and> a + d *\<^sub>R l \<notin> rel_interior S}"
-    proof (rule cInf_greatest [OF nonMT], clarsimp)
-      fix x::real
-      assume "0 < x" and nonrel: "a + x *\<^sub>R l \<notin> rel_interior S"
-      show "d + e / norm l \<le> x"
-      proof (cases "x < d")
-        case True with inint nonrel \<open>0 < x\<close>
-          show ?thesis by auto
-      next
-        case False
-          then have dle: "x < d + e / norm l \<Longrightarrow> dist (a + x *\<^sub>R l) (a + d *\<^sub>R l) < e"
-            by (simp add: field_simps \<open>l \<noteq> 0\<close>)
-          have ain: "a + x *\<^sub>R l \<in> affine hull S"
-            by (metis add_diff_cancel_left' aff affine_affine_hull mem_affine_3_minus aaff)
-          show ?thesis
-            using e [OF ain] nonrel dle by force
-      qed
-    qed
-    then show False
-      using \<open>0 < e\<close> \<open>l \<noteq> 0\<close> by (simp add: d_def [symmetric] divide_simps)
-  qed
-  moreover have "a + d *\<^sub>R l \<in> closure S"
-  proof (clarsimp simp: closure_approachable)
-    fix \<eta>::real assume "0 < \<eta>"
-    have 1: "a + (d - min d (\<eta> / 2 / norm l)) *\<^sub>R l \<in> S"
-      apply (rule subsetD [OF rel_interior_subset inint])
-      using \<open>l \<noteq> 0\<close> \<open>0 < d\<close> \<open>0 < \<eta>\<close> by auto
-    have "norm l * min d (\<eta> / (norm l * 2)) \<le> norm l * (\<eta> / (norm l * 2))"
-      by (metis min_def mult_left_mono norm_ge_zero order_refl)
-    also have "... < \<eta>"
-      using \<open>l \<noteq> 0\<close> \<open>0 < \<eta>\<close> by (simp add: divide_simps)
-    finally have 2: "norm l * min d (\<eta> / (norm l * 2)) < \<eta>" .
-    show "\<exists>y\<in>S. dist y (a + d *\<^sub>R l) < \<eta>"
-      apply (rule_tac x="a + (d - min d (\<eta> / 2 / norm l)) *\<^sub>R l" in bexI)
-      using 1 2 \<open>0 < d\<close> \<open>0 < \<eta>\<close> apply (auto simp: algebra_simps)
-      done
-  qed
-  ultimately have infront: "a + d *\<^sub>R l \<in> rel_frontier S"
-    by (simp add: rel_frontier_def)
-  show ?thesis
-    by (rule that [OF \<open>0 < d\<close> infront inint])
-qed
-
-corollary ray_to_frontier:
-  fixes a :: "'a::euclidean_space"
-  assumes "bounded S"
-      and a: "a \<in> interior S"
-      and "l \<noteq> 0"
-  obtains d where "0 < d" "(a + d *\<^sub>R l) \<in> frontier S"
-           "\<And>e. \<lbrakk>0 \<le> e; e < d\<rbrakk> \<Longrightarrow> (a + e *\<^sub>R l) \<in> interior S"
-proof -
-  have "interior S = rel_interior S"
-    using a rel_interior_nonempty_interior by auto
-  then have "a \<in> rel_interior S"
-    using a by simp
-  then show ?thesis
-    apply (rule ray_to_rel_frontier [OF \<open>bounded S\<close> _ _ \<open>l \<noteq> 0\<close>])
-     using a affine_hull_nonempty_interior apply blast
-    by (simp add: \<open>interior S = rel_interior S\<close> frontier_def rel_frontier_def that)
-qed
-
-
-lemma segment_to_rel_frontier_aux:
-  fixes x :: "'a::euclidean_space"
-  assumes "convex S" "bounded S" and x: "x \<in> rel_interior S" and y: "y \<in> S" and xy: "x \<noteq> y"
-  obtains z where "z \<in> rel_frontier S" "y \<in> closed_segment x z"
-                   "open_segment x z \<subseteq> rel_interior S"
-proof -
-  have "x + (y - x) \<in> affine hull S"
-    using hull_inc [OF y] by auto
-  then obtain d where "0 < d" and df: "(x + d *\<^sub>R (y-x)) \<in> rel_frontier S"
-                  and di: "\<And>e. \<lbrakk>0 \<le> e; e < d\<rbrakk> \<Longrightarrow> (x + e *\<^sub>R (y-x)) \<in> rel_interior S"
-    by (rule ray_to_rel_frontier [OF \<open>bounded S\<close> x]) (use xy in auto)
-  show ?thesis
-  proof
-    show "x + d *\<^sub>R (y - x) \<in> rel_frontier S"
-      by (simp add: df)
-  next
-    have "open_segment x y \<subseteq> rel_interior S"
-      using rel_interior_closure_convex_segment [OF \<open>convex S\<close> x] closure_subset y by blast
-    moreover have "x + d *\<^sub>R (y - x) \<in> open_segment x y" if "d < 1"
-      using xy
-      apply (auto simp: in_segment)
-      apply (rule_tac x="d" in exI)
-      using \<open>0 < d\<close> that apply (auto simp: divide_simps algebra_simps)
-      done
-    ultimately have "1 \<le> d"
-      using df rel_frontier_def by fastforce
-    moreover have "x = (1 / d) *\<^sub>R x + ((d - 1) / d) *\<^sub>R x"
-      by (metis \<open>0 < d\<close> add.commute add_divide_distrib diff_add_cancel divide_self_if less_irrefl scaleR_add_left scaleR_one)
-    ultimately show "y \<in> closed_segment x (x + d *\<^sub>R (y - x))"
-      apply (auto simp: in_segment)
-      apply (rule_tac x="1/d" in exI)
-      apply (auto simp: divide_simps algebra_simps)
-      done
-  next
-    show "open_segment x (x + d *\<^sub>R (y - x)) \<subseteq> rel_interior S"
-      apply (rule rel_interior_closure_convex_segment [OF \<open>convex S\<close> x])
-      using df rel_frontier_def by auto
-  qed
-qed
-
-lemma segment_to_rel_frontier:
-  fixes x :: "'a::euclidean_space"
-  assumes S: "convex S" "bounded S" and x: "x \<in> rel_interior S"
-      and y: "y \<in> S" and xy: "\<not>(x = y \<and> S = {x})"
-  obtains z where "z \<in> rel_frontier S" "y \<in> closed_segment x z"
-                  "open_segment x z \<subseteq> rel_interior S"
-proof (cases "x=y")
-  case True
-  with xy have "S \<noteq> {x}"
-    by blast
-  with True show ?thesis
-    by (metis Set.set_insert all_not_in_conv ends_in_segment(1) insert_iff segment_to_rel_frontier_aux[OF S x] that y)
-next
-  case False
-  then show ?thesis
-    using segment_to_rel_frontier_aux [OF S x y] that by blast
-qed
-
-proposition rel_frontier_not_sing:
-  fixes a :: "'a::euclidean_space"
-  assumes "bounded S"
-    shows "rel_frontier S \<noteq> {a}"
-proof (cases "S = {}")
-  case True  then show ?thesis  by simp
-next
-  case False
-  then obtain z where "z \<in> S"
-    by blast
-  then show ?thesis
-  proof (cases "S = {z}")
-    case True then show ?thesis  by simp
-  next
-    case False
-    then obtain w where "w \<in> S" "w \<noteq> z"
-      using \<open>z \<in> S\<close> by blast
-    show ?thesis
-    proof
-      assume "rel_frontier S = {a}"
-      then consider "w \<notin> rel_frontier S" | "z \<notin> rel_frontier S"
-        using \<open>w \<noteq> z\<close> by auto
-      then show False
-      proof cases
-        case 1
-        then have w: "w \<in> rel_interior S"
-          using \<open>w \<in> S\<close> closure_subset rel_frontier_def by fastforce
-        have "w + (w - z) \<in> affine hull S"
-          by (metis \<open>w \<in> S\<close> \<open>z \<in> S\<close> affine_affine_hull hull_inc mem_affine_3_minus scaleR_one)
-        then obtain e where "0 < e" "(w + e *\<^sub>R (w - z)) \<in> rel_frontier S"
-          using \<open>w \<noteq> z\<close>  \<open>z \<in> S\<close> by (metis assms ray_to_rel_frontier right_minus_eq w)
-        moreover obtain d where "0 < d" "(w + d *\<^sub>R (z - w)) \<in> rel_frontier S"
-          using ray_to_rel_frontier [OF \<open>bounded S\<close> w, of "1 *\<^sub>R (z - w)"]  \<open>w \<noteq> z\<close>  \<open>z \<in> S\<close>
-          by (metis add.commute add.right_neutral diff_add_cancel hull_inc scaleR_one)
-        ultimately have "d *\<^sub>R (z - w) = e *\<^sub>R (w - z)"
-          using \<open>rel_frontier S = {a}\<close> by force
-        moreover have "e \<noteq> -d "
-          using \<open>0 < e\<close> \<open>0 < d\<close> by force
-        ultimately show False
-          by (metis (no_types, lifting) \<open>w \<noteq> z\<close> eq_iff_diff_eq_0 minus_diff_eq real_vector.scale_cancel_right real_vector.scale_minus_right scaleR_left.minus)
-      next
-        case 2
-        then have z: "z \<in> rel_interior S"
-          using \<open>z \<in> S\<close> closure_subset rel_frontier_def by fastforce
-        have "z + (z - w) \<in> affine hull S"
-          by (metis \<open>z \<in> S\<close> \<open>w \<in> S\<close> affine_affine_hull hull_inc mem_affine_3_minus scaleR_one)
-        then obtain e where "0 < e" "(z + e *\<^sub>R (z - w)) \<in> rel_frontier S"
-          using \<open>w \<noteq> z\<close>  \<open>w \<in> S\<close> by (metis assms ray_to_rel_frontier right_minus_eq z)
-        moreover obtain d where "0 < d" "(z + d *\<^sub>R (w - z)) \<in> rel_frontier S"
-          using ray_to_rel_frontier [OF \<open>bounded S\<close> z, of "1 *\<^sub>R (w - z)"]  \<open>w \<noteq> z\<close>  \<open>w \<in> S\<close>
-          by (metis add.commute add.right_neutral diff_add_cancel hull_inc scaleR_one)
-        ultimately have "d *\<^sub>R (w - z) = e *\<^sub>R (z - w)"
-          using \<open>rel_frontier S = {a}\<close> by force
-        moreover have "e \<noteq> -d "
-          using \<open>0 < e\<close> \<open>0 < d\<close> by force
-        ultimately show False
-          by (metis (no_types, lifting) \<open>w \<noteq> z\<close> eq_iff_diff_eq_0 minus_diff_eq real_vector.scale_cancel_right real_vector.scale_minus_right scaleR_left.minus)
-      qed
-    qed
-  qed
-qed
-
 proposition
   fixes S :: "'a::euclidean_space set"
   assumes "compact S" and 0: "0 \<in> rel_interior S"
@@ -1268,6 +1028,20 @@
   using assms
   by (meson zero_less_one homeomorphic_trans homeomorphic_convex_compact_cball homeomorphic_sym)
 
+lemma homeomorphic_closed_intervals:
+  fixes a :: "'a::euclidean_space" and b and c :: "'a::euclidean_space" and d
+  assumes "box a b \<noteq> {}" and "box c d \<noteq> {}"
+    shows "(cbox a b) homeomorphic (cbox c d)"
+apply (rule homeomorphic_convex_compact)
+using assms apply auto
+done
+
+lemma homeomorphic_closed_intervals_real:
+  fixes a::real and b and c::real and d
+  assumes "a<b" and "c<d"
+  shows "{a..b} homeomorphic {c..d}"
+  using assms by (auto intro: homeomorphic_convex_compact)
+
 subsection\<open>Covering spaces and lifting results for them\<close>
 
 definition\<^marker>\<open>tag important\<close> covering_space
diff -r 191bb458b95c -r f95193669ad7 src/HOL/Analysis/Ordered_Euclidean_Space.thy
--- a/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Tue Aug 27 23:12:28 2019 +0200
+++ b/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Wed Aug 28 00:08:14 2019 +0200
@@ -300,20 +300,6 @@
   shows "compact {a .. b}"
   by (metis compact_cbox interval_cbox)
 
-lemma homeomorphic_closed_intervals:
-  fixes a :: "'a::euclidean_space" and b and c :: "'a::euclidean_space" and d
-  assumes "box a b \<noteq> {}" and "box c d \<noteq> {}"
-    shows "(cbox a b) homeomorphic (cbox c d)"
-apply (rule homeomorphic_convex_compact)
-using assms apply auto
-done
-
-lemma homeomorphic_closed_intervals_real:
-  fixes a::real and b and c::real and d
-  assumes "a<b" and "c<d"
-  shows "{a..b} homeomorphic {c..d}"
-  using assms by (auto intro: homeomorphic_convex_compact)
-
 no_notation
   eucl_less (infix "<e" 50)
 
@@ -349,15 +335,5 @@
 
 end
 
-lemma ANR_interval [iff]:
-    fixes a :: "'a::ordered_euclidean_space"
-    shows "ANR{a..b}"
-by (simp add: interval_cbox)
-
-lemma ENR_interval [iff]:
-    fixes a :: "'a::ordered_euclidean_space"
-    shows "ENR{a..b}"
-  by (auto simp: interval_cbox)
-    
 end
 
diff -r 191bb458b95c -r f95193669ad7 src/HOL/Analysis/Starlike.thy
--- a/src/HOL/Analysis/Starlike.thy	Tue Aug 27 23:12:28 2019 +0200
+++ b/src/HOL/Analysis/Starlike.thy	Wed Aug 28 00:08:14 2019 +0200
@@ -3357,6 +3357,246 @@
   then show "?lhs \<supseteq> ?rhs" by blast
 qed
 
+proposition ray_to_rel_frontier:
+  fixes a :: "'a::real_inner"
+  assumes "bounded S"
+      and a: "a \<in> rel_interior S"
+      and aff: "(a + l) \<in> affine hull S"
+      and "l \<noteq> 0"
+  obtains d where "0 < d" "(a + d *\<^sub>R l) \<in> rel_frontier S"
+           "\<And>e. \<lbrakk>0 \<le> e; e < d\<rbrakk> \<Longrightarrow> (a + e *\<^sub>R l) \<in> rel_interior S"
+proof -
+  have aaff: "a \<in> affine hull S"
+    by (meson a hull_subset rel_interior_subset rev_subsetD)
+  let ?D = "{d. 0 < d \<and> a + d *\<^sub>R l \<notin> rel_interior S}"
+  obtain B where "B > 0" and B: "S \<subseteq> ball a B"
+    using bounded_subset_ballD [OF \<open>bounded S\<close>] by blast
+  have "a + (B / norm l) *\<^sub>R l \<notin> ball a B"
+    by (simp add: dist_norm \<open>l \<noteq> 0\<close>)
+  with B have "a + (B / norm l) *\<^sub>R l \<notin> rel_interior S"
+    using rel_interior_subset subsetCE by blast
+  with \<open>B > 0\<close> \<open>l \<noteq> 0\<close> have nonMT: "?D \<noteq> {}"
+    using divide_pos_pos zero_less_norm_iff by fastforce
+  have bdd: "bdd_below ?D"
+    by (metis (no_types, lifting) bdd_belowI le_less mem_Collect_eq)
+  have relin_Ex: "\<And>x. x \<in> rel_interior S \<Longrightarrow>
+                    \<exists>e>0. \<forall>x'\<in>affine hull S. dist x' x < e \<longrightarrow> x' \<in> rel_interior S"
+    using openin_rel_interior [of S] by (simp add: openin_euclidean_subtopology_iff)
+  define d where "d = Inf ?D"
+  obtain \<epsilon> where "0 < \<epsilon>" and \<epsilon>: "\<And>\<eta>. \<lbrakk>0 \<le> \<eta>; \<eta> < \<epsilon>\<rbrakk> \<Longrightarrow> (a + \<eta> *\<^sub>R l) \<in> rel_interior S"
+  proof -
+    obtain e where "e>0"
+            and e: "\<And>x'. x' \<in> affine hull S \<Longrightarrow> dist x' a < e \<Longrightarrow> x' \<in> rel_interior S"
+      using relin_Ex a by blast
+    show thesis
+    proof (rule_tac \<epsilon> = "e / norm l" in that)
+      show "0 < e / norm l" by (simp add: \<open>0 < e\<close> \<open>l \<noteq> 0\<close>)
+    next
+      show "a + \<eta> *\<^sub>R l \<in> rel_interior S" if "0 \<le> \<eta>" "\<eta> < e / norm l" for \<eta>
+      proof (rule e)
+        show "a + \<eta> *\<^sub>R l \<in> affine hull S"
+          by (metis (no_types) add_diff_cancel_left' aff affine_affine_hull mem_affine_3_minus aaff)
+        show "dist (a + \<eta> *\<^sub>R l) a < e"
+          using that by (simp add: \<open>l \<noteq> 0\<close> dist_norm pos_less_divide_eq)
+      qed
+    qed
+  qed
+  have inint: "\<And>e. \<lbrakk>0 \<le> e; e < d\<rbrakk> \<Longrightarrow> a + e *\<^sub>R l \<in> rel_interior S"
+    unfolding d_def using cInf_lower [OF _ bdd]
+    by (metis (no_types, lifting) a add.right_neutral le_less mem_Collect_eq not_less real_vector.scale_zero_left)
+  have "\<epsilon> \<le> d"
+    unfolding d_def
+    apply (rule cInf_greatest [OF nonMT])
+    using \<epsilon> dual_order.strict_implies_order le_less_linear by blast
+  with \<open>0 < \<epsilon>\<close> have "0 < d" by simp
+  have "a + d *\<^sub>R l \<notin> rel_interior S"
+  proof
+    assume adl: "a + d *\<^sub>R l \<in> rel_interior S"
+    obtain e where "e > 0"
+             and e: "\<And>x'. x' \<in> affine hull S \<Longrightarrow> dist x' (a + d *\<^sub>R l) < e \<Longrightarrow> x' \<in> rel_interior S"
+      using relin_Ex adl by blast
+    have "d + e / norm l \<le> Inf {d. 0 < d \<and> a + d *\<^sub>R l \<notin> rel_interior S}"
+    proof (rule cInf_greatest [OF nonMT], clarsimp)
+      fix x::real
+      assume "0 < x" and nonrel: "a + x *\<^sub>R l \<notin> rel_interior S"
+      show "d + e / norm l \<le> x"
+      proof (cases "x < d")
+        case True with inint nonrel \<open>0 < x\<close>
+          show ?thesis by auto
+      next
+        case False
+          then have dle: "x < d + e / norm l \<Longrightarrow> dist (a + x *\<^sub>R l) (a + d *\<^sub>R l) < e"
+            by (simp add: field_simps \<open>l \<noteq> 0\<close>)
+          have ain: "a + x *\<^sub>R l \<in> affine hull S"
+            by (metis add_diff_cancel_left' aff affine_affine_hull mem_affine_3_minus aaff)
+          show ?thesis
+            using e [OF ain] nonrel dle by force
+      qed
+    qed
+    then show False
+      using \<open>0 < e\<close> \<open>l \<noteq> 0\<close> by (simp add: d_def [symmetric] divide_simps)
+  qed
+  moreover have "a + d *\<^sub>R l \<in> closure S"
+  proof (clarsimp simp: closure_approachable)
+    fix \<eta>::real assume "0 < \<eta>"
+    have 1: "a + (d - min d (\<eta> / 2 / norm l)) *\<^sub>R l \<in> S"
+      apply (rule subsetD [OF rel_interior_subset inint])
+      using \<open>l \<noteq> 0\<close> \<open>0 < d\<close> \<open>0 < \<eta>\<close> by auto
+    have "norm l * min d (\<eta> / (norm l * 2)) \<le> norm l * (\<eta> / (norm l * 2))"
+      by (metis min_def mult_left_mono norm_ge_zero order_refl)
+    also have "... < \<eta>"
+      using \<open>l \<noteq> 0\<close> \<open>0 < \<eta>\<close> by (simp add: divide_simps)
+    finally have 2: "norm l * min d (\<eta> / (norm l * 2)) < \<eta>" .
+    show "\<exists>y\<in>S. dist y (a + d *\<^sub>R l) < \<eta>"
+      apply (rule_tac x="a + (d - min d (\<eta> / 2 / norm l)) *\<^sub>R l" in bexI)
+      using 1 2 \<open>0 < d\<close> \<open>0 < \<eta>\<close> apply (auto simp: algebra_simps)
+      done
+  qed
+  ultimately have infront: "a + d *\<^sub>R l \<in> rel_frontier S"
+    by (simp add: rel_frontier_def)
+  show ?thesis
+    by (rule that [OF \<open>0 < d\<close> infront inint])
+qed
+
+corollary ray_to_frontier:
+  fixes a :: "'a::euclidean_space"
+  assumes "bounded S"
+      and a: "a \<in> interior S"
+      and "l \<noteq> 0"
+  obtains d where "0 < d" "(a + d *\<^sub>R l) \<in> frontier S"
+           "\<And>e. \<lbrakk>0 \<le> e; e < d\<rbrakk> \<Longrightarrow> (a + e *\<^sub>R l) \<in> interior S"
+proof -
+  have "interior S = rel_interior S"
+    using a rel_interior_nonempty_interior by auto
+  then have "a \<in> rel_interior S"
+    using a by simp
+  then show ?thesis
+    apply (rule ray_to_rel_frontier [OF \<open>bounded S\<close> _ _ \<open>l \<noteq> 0\<close>])
+     using a affine_hull_nonempty_interior apply blast
+    by (simp add: \<open>interior S = rel_interior S\<close> frontier_def rel_frontier_def that)
+qed
+
+
+lemma segment_to_rel_frontier_aux:
+  fixes x :: "'a::euclidean_space"
+  assumes "convex S" "bounded S" and x: "x \<in> rel_interior S" and y: "y \<in> S" and xy: "x \<noteq> y"
+  obtains z where "z \<in> rel_frontier S" "y \<in> closed_segment x z"
+                   "open_segment x z \<subseteq> rel_interior S"
+proof -
+  have "x + (y - x) \<in> affine hull S"
+    using hull_inc [OF y] by auto
+  then obtain d where "0 < d" and df: "(x + d *\<^sub>R (y-x)) \<in> rel_frontier S"
+                  and di: "\<And>e. \<lbrakk>0 \<le> e; e < d\<rbrakk> \<Longrightarrow> (x + e *\<^sub>R (y-x)) \<in> rel_interior S"
+    by (rule ray_to_rel_frontier [OF \<open>bounded S\<close> x]) (use xy in auto)
+  show ?thesis
+  proof
+    show "x + d *\<^sub>R (y - x) \<in> rel_frontier S"
+      by (simp add: df)
+  next
+    have "open_segment x y \<subseteq> rel_interior S"
+      using rel_interior_closure_convex_segment [OF \<open>convex S\<close> x] closure_subset y by blast
+    moreover have "x + d *\<^sub>R (y - x) \<in> open_segment x y" if "d < 1"
+      using xy
+      apply (auto simp: in_segment)
+      apply (rule_tac x="d" in exI)
+      using \<open>0 < d\<close> that apply (auto simp: divide_simps algebra_simps)
+      done
+    ultimately have "1 \<le> d"
+      using df rel_frontier_def by fastforce
+    moreover have "x = (1 / d) *\<^sub>R x + ((d - 1) / d) *\<^sub>R x"
+      by (metis \<open>0 < d\<close> add.commute add_divide_distrib diff_add_cancel divide_self_if less_irrefl scaleR_add_left scaleR_one)
+    ultimately show "y \<in> closed_segment x (x + d *\<^sub>R (y - x))"
+      apply (auto simp: in_segment)
+      apply (rule_tac x="1/d" in exI)
+      apply (auto simp: divide_simps algebra_simps)
+      done
+  next
+    show "open_segment x (x + d *\<^sub>R (y - x)) \<subseteq> rel_interior S"
+      apply (rule rel_interior_closure_convex_segment [OF \<open>convex S\<close> x])
+      using df rel_frontier_def by auto
+  qed
+qed
+
+lemma segment_to_rel_frontier:
+  fixes x :: "'a::euclidean_space"
+  assumes S: "convex S" "bounded S" and x: "x \<in> rel_interior S"
+      and y: "y \<in> S" and xy: "\<not>(x = y \<and> S = {x})"
+  obtains z where "z \<in> rel_frontier S" "y \<in> closed_segment x z"
+                  "open_segment x z \<subseteq> rel_interior S"
+proof (cases "x=y")
+  case True
+  with xy have "S \<noteq> {x}"
+    by blast
+  with True show ?thesis
+    by (metis Set.set_insert all_not_in_conv ends_in_segment(1) insert_iff segment_to_rel_frontier_aux[OF S x] that y)
+next
+  case False
+  then show ?thesis
+    using segment_to_rel_frontier_aux [OF S x y] that by blast
+qed
+
+proposition rel_frontier_not_sing:
+  fixes a :: "'a::euclidean_space"
+  assumes "bounded S"
+    shows "rel_frontier S \<noteq> {a}"
+proof (cases "S = {}")
+  case True  then show ?thesis  by simp
+next
+  case False
+  then obtain z where "z \<in> S"
+    by blast
+  then show ?thesis
+  proof (cases "S = {z}")
+    case True then show ?thesis  by simp
+  next
+    case False
+    then obtain w where "w \<in> S" "w \<noteq> z"
+      using \<open>z \<in> S\<close> by blast
+    show ?thesis
+    proof
+      assume "rel_frontier S = {a}"
+      then consider "w \<notin> rel_frontier S" | "z \<notin> rel_frontier S"
+        using \<open>w \<noteq> z\<close> by auto
+      then show False
+      proof cases
+        case 1
+        then have w: "w \<in> rel_interior S"
+          using \<open>w \<in> S\<close> closure_subset rel_frontier_def by fastforce
+        have "w + (w - z) \<in> affine hull S"
+          by (metis \<open>w \<in> S\<close> \<open>z \<in> S\<close> affine_affine_hull hull_inc mem_affine_3_minus scaleR_one)
+        then obtain e where "0 < e" "(w + e *\<^sub>R (w - z)) \<in> rel_frontier S"
+          using \<open>w \<noteq> z\<close>  \<open>z \<in> S\<close> by (metis assms ray_to_rel_frontier right_minus_eq w)
+        moreover obtain d where "0 < d" "(w + d *\<^sub>R (z - w)) \<in> rel_frontier S"
+          using ray_to_rel_frontier [OF \<open>bounded S\<close> w, of "1 *\<^sub>R (z - w)"]  \<open>w \<noteq> z\<close>  \<open>z \<in> S\<close>
+          by (metis add.commute add.right_neutral diff_add_cancel hull_inc scaleR_one)
+        ultimately have "d *\<^sub>R (z - w) = e *\<^sub>R (w - z)"
+          using \<open>rel_frontier S = {a}\<close> by force
+        moreover have "e \<noteq> -d "
+          using \<open>0 < e\<close> \<open>0 < d\<close> by force
+        ultimately show False
+          by (metis (no_types, lifting) \<open>w \<noteq> z\<close> eq_iff_diff_eq_0 minus_diff_eq real_vector.scale_cancel_right real_vector.scale_minus_right scaleR_left.minus)
+      next
+        case 2
+        then have z: "z \<in> rel_interior S"
+          using \<open>z \<in> S\<close> closure_subset rel_frontier_def by fastforce
+        have "z + (z - w) \<in> affine hull S"
+          by (metis \<open>z \<in> S\<close> \<open>w \<in> S\<close> affine_affine_hull hull_inc mem_affine_3_minus scaleR_one)
+        then obtain e where "0 < e" "(z + e *\<^sub>R (z - w)) \<in> rel_frontier S"
+          using \<open>w \<noteq> z\<close>  \<open>w \<in> S\<close> by (metis assms ray_to_rel_frontier right_minus_eq z)
+        moreover obtain d where "0 < d" "(z + d *\<^sub>R (w - z)) \<in> rel_frontier S"
+          using ray_to_rel_frontier [OF \<open>bounded S\<close> z, of "1 *\<^sub>R (w - z)"]  \<open>w \<noteq> z\<close>  \<open>w \<in> S\<close>
+          by (metis add.commute add.right_neutral diff_add_cancel hull_inc scaleR_one)
+        ultimately have "d *\<^sub>R (w - z) = e *\<^sub>R (z - w)"
+          using \<open>rel_frontier S = {a}\<close> by force
+        moreover have "e \<noteq> -d "
+          using \<open>0 < e\<close> \<open>0 < d\<close> by force
+        ultimately show False
+          by (metis (no_types, lifting) \<open>w \<noteq> z\<close> eq_iff_diff_eq_0 minus_diff_eq real_vector.scale_cancel_right real_vector.scale_minus_right scaleR_left.minus)
+      qed
+    qed
+  qed
+qed
+
 
 subsection\<^marker>\<open>tag unimportant\<close> \<open>Convexity on direct sums\<close>