two new lemmas about segments
authorpaulson <lp15@cam.ac.uk>
Tue May 10 11:56:23 2016 +0100 (2016-05-10 ago)
changeset 63077844725394a37
parent 63076 1e771f0db448
child 63078 e49dc94eb624
two new lemmas about segments
src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
     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.19 +  by (force simp add: in_segment linear_add_cmul)
    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: