equal
deleted
inserted
replaced
394 unfolding hull_def using affine_Inter[of "{t \<in> affine. s \<subseteq> t}"] |
394 unfolding hull_def using affine_Inter[of "{t \<in> affine. s \<subseteq> t}"] |
395 unfolding mem_def by auto |
395 unfolding mem_def by auto |
396 |
396 |
397 lemma affine_hull_eq[simp]: "(affine hull s = s) \<longleftrightarrow> affine s" |
397 lemma affine_hull_eq[simp]: "(affine hull s = s) \<longleftrightarrow> affine s" |
398 by (metis affine_affine_hull hull_same mem_def) |
398 by (metis affine_affine_hull hull_same mem_def) |
399 |
|
400 lemma setsum_restrict_set'': assumes "finite A" |
|
401 shows "setsum f {x \<in> A. P x} = (\<Sum>x\<in>A. if P x then f x else 0)" |
|
402 unfolding mem_def[of _ P, symmetric] unfolding setsum_restrict_set'[OF assms] .. |
|
403 |
399 |
404 subsection {* Some explicit formulations (from Lars Schewe). *} |
400 subsection {* Some explicit formulations (from Lars Schewe). *} |
405 |
401 |
406 lemma affine: fixes V::"'a::real_vector set" |
402 lemma affine: fixes V::"'a::real_vector set" |
407 shows "affine V \<longleftrightarrow> (\<forall>s u. finite s \<and> s \<noteq> {} \<and> s \<subseteq> V \<and> setsum u s = 1 \<longrightarrow> (setsum (\<lambda>x. (u x) *\<^sub>R x)) s \<in> V)" |
403 shows "affine V \<longleftrightarrow> (\<forall>s u. finite s \<and> s \<noteq> {} \<and> s \<subseteq> V \<and> setsum u s = 1 \<longrightarrow> (setsum (\<lambda>x. (u x) *\<^sub>R x)) s \<in> V)" |