equal
deleted
inserted
replaced
7055 finally show "setsum (op \<bullet> ?a) ?D < 1" by auto |
7055 finally show "setsum (op \<bullet> ?a) ?D < 1" by auto |
7056 next |
7056 next |
7057 fix i |
7057 fix i |
7058 assume "i \<in> Basis" and "i \<notin> d" |
7058 assume "i \<in> Basis" and "i \<notin> d" |
7059 have "?a \<in> span d" |
7059 have "?a \<in> span d" |
7060 apply (rule span_setsum[of d "(\<lambda>b. b /\<^sub>R (2 * real (card d)))" d]) |
7060 proof (rule span_setsum[of d "(\<lambda>b. b /\<^sub>R (2 * real (card d)))" d]) |
7061 using finite_subset[OF assms(2) finite_Basis] |
|
7062 apply blast |
|
7063 proof - |
|
7064 { |
7061 { |
7065 fix x :: "'a::euclidean_space" |
7062 fix x :: "'a::euclidean_space" |
7066 assume "x \<in> d" |
7063 assume "x \<in> d" |
7067 then have "x \<in> span d" |
7064 then have "x \<in> span d" |
7068 using span_superset[of _ "d"] by auto |
7065 using span_superset[of _ "d"] by auto |