equal
deleted
inserted
replaced
3092 by(simp only: image_image[THEN sym] convex_hull_scaling convex_hull_translation) |
3092 by(simp only: image_image[THEN sym] convex_hull_scaling convex_hull_translation) |
3093 |
3093 |
3094 subsection {* Convexity of cone hulls *} |
3094 subsection {* Convexity of cone hulls *} |
3095 |
3095 |
3096 lemma convex_cone_hull: |
3096 lemma convex_cone_hull: |
3097 fixes S :: "('m::euclidean_space) set" |
|
3098 assumes "convex S" |
3097 assumes "convex S" |
3099 shows "convex (cone hull S)" |
3098 shows "convex (cone hull S)" |
3100 proof- |
3099 proof- |
3101 { fix x y assume xy_def: "x : cone hull S & y : cone hull S" |
3100 { fix x y assume xy_def: "x : cone hull S & y : cone hull S" |
3102 hence "S ~= {}" using cone_hull_empty_iff[of S] by auto |
3101 hence "S ~= {}" using cone_hull_empty_iff[of S] by auto |