equal
deleted
inserted
replaced
103 apply (subst euclidean_representation_setsum_fun [symmetric]) |
103 apply (subst euclidean_representation_setsum_fun [symmetric]) |
104 apply (rule isCont_setsum) |
104 apply (rule isCont_setsum) |
105 apply (blast intro: assms) |
105 apply (blast intro: assms) |
106 done |
106 done |
107 |
107 |
108 lemma DIM_positive: "0 < DIM('a::euclidean_space)" |
108 lemma DIM_positive [simp]: "0 < DIM('a::euclidean_space)" |
109 by (simp add: card_gt_0_iff) |
109 by (simp add: card_gt_0_iff) |
110 |
110 |
111 lemma DIM_ge_Suc0 [iff]: "Suc 0 \<le> card Basis" |
111 lemma DIM_ge_Suc0 [simp]: "Suc 0 \<le> card Basis" |
112 by (meson DIM_positive Suc_leI) |
112 by (meson DIM_positive Suc_leI) |
113 |
113 |
114 |
114 |
115 lemma setsum_inner_Basis_scaleR [simp]: |
115 lemma setsum_inner_Basis_scaleR [simp]: |
116 fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_vector" |
116 fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_vector" |