--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Mon Dec 16 17:08:22 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Mon Dec 16 17:08:22 2013 +0100
@@ -7,7 +7,7 @@
theory Convex_Euclidean_Space
imports
- Topology_Euclidean_Space
+ Ordered_Euclidean_Space
"~~/src/HOL/Library/Convex"
"~~/src/HOL/Library/Set_Algebras"
begin
@@ -343,11 +343,6 @@
lemma if_smult: "(if P then x else (y::real)) *\<^sub>R v = (if P then x *\<^sub>R v else y *\<^sub>R v)"
by auto
-lemma image_smult_interval:
- "(\<lambda>x. m *\<^sub>R (x::'a::ordered_euclidean_space)) ` {a..b} =
- (if {a..b} = {} then {} else if 0 \<le> m then {m *\<^sub>R a..m *\<^sub>R b} else {m *\<^sub>R b..m *\<^sub>R a})"
- using image_affinity_interval[of m 0 a b] by auto
-
lemma dist_triangle_eq:
fixes x y z :: "'a::real_inner"
shows "dist x z = dist x y + dist y z \<longleftrightarrow>