--- a/src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy	Tue Jul 12 22:54:37 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy	Wed Jul 13 17:14:17 2016 +0100
@@ -293,5 +293,15 @@
 
 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