src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy

--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Dec 21 19:08:26 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Dec 22 14:33:34 2015 +0000
@@ -855,6 +855,9 @@
 lemma ball_subset_cball [simp,intro]: "ball x e \<subseteq> cball x e"
   by (simp add: subset_eq)
 
+lemma sphere_cball [simp,intro]: "sphere z r \<subseteq> cball z r"
+  by force
+
 lemma subset_ball[intro]: "d \<le> e \<Longrightarrow> ball x d \<subseteq> ball x e"
   by (simp add: subset_eq)