equal
deleted
inserted
replaced
383 assumes "convex s" |
383 assumes "convex s" |
384 shows "convex ((\<lambda>x. c *\<^sub>R x) ` s)" |
384 shows "convex ((\<lambda>x. c *\<^sub>R x) ` s)" |
385 proof - |
385 proof - |
386 have "linear (\<lambda>x. c *\<^sub>R x)" |
386 have "linear (\<lambda>x. c *\<^sub>R x)" |
387 by (simp add: linearI scaleR_add_right) |
387 by (simp add: linearI scaleR_add_right) |
|
388 then show ?thesis |
|
389 using `convex s` by (rule convex_linear_image) |
|
390 qed |
|
391 |
|
392 lemma convex_scaled: |
|
393 assumes "convex s" |
|
394 shows "convex ((\<lambda>x. x *\<^sub>R c) ` s)" |
|
395 proof - |
|
396 have "linear (\<lambda>x. x *\<^sub>R c)" |
|
397 by (simp add: linearI scaleR_add_left) |
388 then show ?thesis |
398 then show ?thesis |
389 using `convex s` by (rule convex_linear_image) |
399 using `convex s` by (rule convex_linear_image) |
390 qed |
400 qed |
391 |
401 |
392 lemma convex_negations: |
402 lemma convex_negations: |