author paulson Tue May 10 11:56:23 2016 +0100 (2016-05-10 ago) changeset 63077 844725394a37 parent 63076 1e771f0db448 child 63078 e49dc94eb624
1.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon May 09 17:32:26 2016 +0100
1.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Tue May 10 11:56:23 2016 +0100
1.3 @@ -6546,9 +6546,6 @@
1.5  subsection \<open>Line segments, Starlike Sets, etc.\<close>
1.7 -(* Use the same overloading tricks as for intervals, so that
1.8 -   segment[a,b] is closed and segment(a,b) is open relative to affine hull. *)
1.9 -
1.10  definition midpoint :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a"
1.11    where "midpoint a b = (inverse (2::real)) *\<^sub>R (a + b)"
1.13 @@ -6565,9 +6562,17 @@
1.14      "x \<in> open_segment a b \<longleftrightarrow> a \<noteq> b \<and> (\<exists>u. 0 < u \<and> u < 1 \<and> x = (1 - u) *\<^sub>R a + u *\<^sub>R b)"
1.15    using less_eq_real_def by (auto simp: segment algebra_simps)
1.17 +lemma closed_segment_linear_image:
1.18 +    "linear f \<Longrightarrow> closed_segment (f a) (f b) = f ` (closed_segment a b)"