equal
deleted
inserted
replaced
1254 "\<exists>u. x = (\<Sum>v\<in>basis ` {..<DIM('a)}. u v *\<^sub>R (v\<Colon>'a\<Colon>euclidean_space))" |
1254 "\<exists>u. x = (\<Sum>v\<in>basis ` {..<DIM('a)}. u v *\<^sub>R (v\<Colon>'a\<Colon>euclidean_space))" |
1255 proof - |
1255 proof - |
1256 have "x\<in>UNIV" by auto from this[unfolded span_basis[THEN sym]] |
1256 have "x\<in>UNIV" by auto from this[unfolded span_basis[THEN sym]] |
1257 have "\<exists>u. (\<Sum>v\<in>basis ` {..<DIM('a)}. u v *\<^sub>R v) = x" |
1257 have "\<exists>u. (\<Sum>v\<in>basis ` {..<DIM('a)}. u v *\<^sub>R v) = x" |
1258 unfolding range_basis span_insert_0 apply(subst (asm) span_finite) by auto |
1258 unfolding range_basis span_insert_0 apply(subst (asm) span_finite) by auto |
1259 thus ?thesis by fastsimp |
1259 thus ?thesis by fastforce |
1260 qed |
1260 qed |
1261 |
1261 |
1262 lemma span_basis'[simp]:"span ((basis::nat=>'a) ` {..<DIM('a::euclidean_space)}) = UNIV" |
1262 lemma span_basis'[simp]:"span ((basis::nat=>'a) ` {..<DIM('a::euclidean_space)}) = UNIV" |
1263 apply(subst span_basis[symmetric]) unfolding range_basis by auto |
1263 apply(subst span_basis[symmetric]) unfolding range_basis by auto |
1264 |
1264 |