src/HOL/Analysis/Topology_Euclidean_Space.thy

 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"