src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy

     inner_Basis_SUP_left eucl_le[where 'a='a] less_le_not_le abs_vec_def abs_inner)
   done
 
 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