src/HOL/Library/Convex.thy
changeset 53596 d29d63460d84
parent 51642 400ec5ae7f8f
child 53620 3c7f5e7926dc
     1.1 --- a/src/HOL/Library/Convex.thy	Thu Sep 12 09:06:46 2013 -0700
     1.2 +++ b/src/HOL/Library/Convex.thy	Thu Sep 12 09:33:36 2013 -0700
     1.3 @@ -46,6 +46,12 @@
     1.4  lemma convex_Int: "convex s \<Longrightarrow> convex t \<Longrightarrow> convex (s \<inter> t)"
     1.5    unfolding convex_def by auto
     1.6  
     1.7 +lemma convex_INT: "\<forall>i\<in>A. convex (B i) \<Longrightarrow> convex (\<Inter>i\<in>A. B i)"
     1.8 +  unfolding convex_def by auto
     1.9 +
    1.10 +lemma convex_Times: "convex s \<Longrightarrow> convex t \<Longrightarrow> convex (s \<times> t)"
    1.11 +  unfolding convex_def by auto
    1.12 +
    1.13  lemma convex_halfspace_le: "convex {x. inner a x \<le> b}"
    1.14    unfolding convex_def
    1.15    by (auto simp: inner_add intro!: convex_bound_le)