equal
deleted
inserted
replaced
2537 |
2537 |
2538 lemma open_convex_hull[intro]: |
2538 lemma open_convex_hull[intro]: |
2539 fixes s :: "'a::real_normed_vector set" |
2539 fixes s :: "'a::real_normed_vector set" |
2540 assumes "open s" |
2540 assumes "open s" |
2541 shows "open(convex hull s)" |
2541 shows "open(convex hull s)" |
2542 unfolding open_contains_cball convex_hull_explicit unfolding mem_Collect_eq ball_simps(10) |
2542 unfolding open_contains_cball convex_hull_explicit unfolding mem_Collect_eq ball_simps(8) |
2543 proof(rule, rule) fix a |
2543 proof(rule, rule) fix a |
2544 assume "\<exists>sa u. finite sa \<and> sa \<subseteq> s \<and> (\<forall>x\<in>sa. 0 \<le> u x) \<and> setsum u sa = 1 \<and> (\<Sum>v\<in>sa. u v *\<^sub>R v) = a" |
2544 assume "\<exists>sa u. finite sa \<and> sa \<subseteq> s \<and> (\<forall>x\<in>sa. 0 \<le> u x) \<and> setsum u sa = 1 \<and> (\<Sum>v\<in>sa. u v *\<^sub>R v) = a" |
2545 then obtain t u where obt:"finite t" "t\<subseteq>s" "\<forall>x\<in>t. 0 \<le> u x" "setsum u t = 1" "(\<Sum>v\<in>t. u v *\<^sub>R v) = a" by auto |
2545 then obtain t u where obt:"finite t" "t\<subseteq>s" "\<forall>x\<in>t. 0 \<le> u x" "setsum u t = 1" "(\<Sum>v\<in>t. u v *\<^sub>R v) = a" by auto |
2546 |
2546 |
2547 from assms[unfolded open_contains_cball] obtain b where b:"\<forall>x\<in>s. 0 < b x \<and> cball x (b x) \<subseteq> s" |
2547 from assms[unfolded open_contains_cball] obtain b where b:"\<forall>x\<in>s. 0 < b x \<and> cball x (b x) \<subseteq> s" |