src/HOL/Library/Convex.thy
changeset 61426 d53db136e8fd
parent 61070 b72a990adfe2
child 61518 ff12606337e9
     1.1 --- a/src/HOL/Library/Convex.thy	Tue Oct 13 09:21:21 2015 +0200
     1.2 +++ b/src/HOL/Library/Convex.thy	Tue Oct 13 12:42:08 2015 +0100
     1.3 @@ -43,7 +43,7 @@
     1.4      unfolding convex_def by auto
     1.5  qed (auto simp: convex_def)
     1.6  
     1.7 -lemma mem_convex:
     1.8 +lemma convexD_alt:
     1.9    assumes "convex s" "a \<in> s" "b \<in> s" "0 \<le> u" "u \<le> 1"
    1.10    shows "((1 - u) *\<^sub>R a + u *\<^sub>R b) \<in> s"
    1.11    using assms unfolding convex_alt by auto