equal
deleted
inserted
replaced
186 lemma vec_nth_real_1_iff_cbox [simp]: |
186 lemma vec_nth_real_1_iff_cbox [simp]: |
187 fixes a b :: real |
187 fixes a b :: real |
188 shows "(\<lambda>x::real^1. x $ 1) ` S = {a..b} \<longleftrightarrow> S = cbox (vec a) (vec b)" |
188 shows "(\<lambda>x::real^1. x $ 1) ` S = {a..b} \<longleftrightarrow> S = cbox (vec a) (vec b)" |
189 by (metis interval_cbox vec_nth_1_iff_cbox) |
189 by (metis interval_cbox vec_nth_1_iff_cbox) |
190 |
190 |
|
191 lemma sums_vec_nth : |
|
192 assumes "f sums a" |
|
193 shows "(\<lambda>x. f x $ i) sums a $ i" |
|
194 using assms unfolding sums_def |
|
195 by (auto dest: tendsto_vec_nth [where i=i]) |
|
196 |
|
197 lemma summable_vec_nth : |
|
198 assumes "summable f" |
|
199 shows "summable (\<lambda>x. f x $ i)" |
|
200 using assms unfolding summable_def |
|
201 by (blast intro: sums_vec_nth) |
|
202 |
191 lemma closed_eucl_atLeastAtMost[simp, intro]: |
203 lemma closed_eucl_atLeastAtMost[simp, intro]: |
192 fixes a :: "'a::ordered_euclidean_space" |
204 fixes a :: "'a::ordered_euclidean_space" |
193 shows "closed {a..b}" |
205 shows "closed {a..b}" |
194 by (simp add: cbox_interval[symmetric] closed_cbox) |
206 by (simp add: cbox_interval[symmetric] closed_cbox) |
195 |
207 |