diff -r ad2c5f37f659 -r 141e1ed8d5a0 src/HOL/Analysis/Homeomorphism.thy
--- a/src/HOL/Analysis/Homeomorphism.thy	Tue Oct 25 11:55:38 2016 +0200
+++ b/src/HOL/Analysis/Homeomorphism.thy	Tue Oct 25 15:46:07 2016 +0100
@@ -129,6 +129,68 @@
     by (simp add: \<open>interior S = rel_interior S\<close> frontier_def rel_frontier_def that)
 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"