--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Mon Dec 14 14:05:31 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Tue Dec 15 14:40:36 2015 +0000
@@ -6359,6 +6359,9 @@
"convex s \<longleftrightarrow> (\<forall>a\<in>s. \<forall>b\<in>s. closed_segment a b \<subseteq> s)"
unfolding convex_alt closed_segment_def by auto
+lemma closed_segment_subset: "\<lbrakk>x \<in> s; y \<in> s; convex s\<rbrakk> \<Longrightarrow> closed_segment x y \<subseteq> s"
+ by (simp add: convex_contains_segment)
+
lemma closed_segment_subset_convex_hull:
"\<lbrakk>x \<in> convex hull s; y \<in> convex hull s\<rbrakk> \<Longrightarrow> closed_segment x y \<subseteq> convex hull s"
using convex_contains_segment by blast