diff -r 19f3d4af7a7d -r 6440577e34ee src/HOL/Analysis/Homeomorphism.thy
--- a/src/HOL/Analysis/Homeomorphism.thy	Thu Jan 05 14:18:24 2017 +0000
+++ b/src/HOL/Analysis/Homeomorphism.thy	Thu Jan 05 15:03:37 2017 +0000
@@ -8,6 +8,34 @@
 imports Path_Connected
 begin
 
+lemma homeomorphic_spheres':
+  fixes a ::"'a::euclidean_space" and b ::"'b::euclidean_space"
+  assumes "0 < \<delta>" and dimeq: "DIM('a) = DIM('b)"
+  shows "(sphere a \<delta>) homeomorphic (sphere b \<delta>)"
+proof -
+  obtain f :: "'a\<Rightarrow>'b" and g where "linear f" "linear g"
+     and fg: "\<And>x. norm(f x) = norm x" "\<And>y. norm(g y) = norm y" "\<And>x. g(f x) = x" "\<And>y. f(g y) = y"
+    by (blast intro: isomorphisms_UNIV_UNIV [OF dimeq])
+  then have "continuous_on UNIV f" "continuous_on UNIV g"
+    using linear_continuous_on linear_linear by blast+
+  then show ?thesis
+    unfolding homeomorphic_minimal
+    apply(rule_tac x="\<lambda>x. b + f(x - a)" in exI)
+    apply(rule_tac x="\<lambda>x. a + g(x - b)" in exI)
+    using assms
+    apply (force intro: continuous_intros
+                  continuous_on_compose2 [of _ f] continuous_on_compose2 [of _ g] simp: dist_commute dist_norm fg)
+    done
+qed
+
+lemma homeomorphic_spheres_gen:
+    fixes a :: "'a::euclidean_space" and b :: "'b::euclidean_space"
+  assumes "0 < r" "0 < s" "DIM('a::euclidean_space) = DIM('b::euclidean_space)"
+  shows "(sphere a r homeomorphic sphere b s)"
+  apply (rule homeomorphic_trans [OF homeomorphic_spheres homeomorphic_spheres'])
+  using assms  apply auto
+  done
+
 subsection \<open>Homeomorphism of all convex compact sets with nonempty interior\<close>
 
 proposition ray_to_rel_frontier: