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.4
1.5  subsection \<open>Line segments, Starlike Sets, etc.\<close>
1.6
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.12
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.16
1.17 +lemma closed_segment_linear_image:
1.18 +    "linear f \<Longrightarrow> closed_segment (f a) (f b) = f ` (closed_segment a b)"
1.20 +
1.21 +lemma open_segment_linear_image:
1.22 +    "\<lbrakk>linear f; inj f\<rbrakk> \<Longrightarrow> open_segment (f a) (f b) = f ` (open_segment a b)"
1.23 +  by (force simp: open_segment_def closed_segment_linear_image inj_on_def)
1.24 +
1.25  lemma open_segment_PairD:
1.26 -  "(x, x') \<in> open_segment (a, a') (b, b')
1.27 -  \<Longrightarrow> (x \<in> open_segment a b \<or> a = b) \<and> (x' \<in> open_segment a' b' \<or> a' = b')"
1.28 +    "(x, x') \<in> open_segment (a, a') (b, b')
1.29 +     \<Longrightarrow> (x \<in> open_segment a b \<or> a = b) \<and> (x' \<in> open_segment a' b' \<or> a' = b')"
1.30    by (auto simp: in_segment)
1.31
1.32  lemma closed_segment_PairD:
```