241 eucl_less (infix "<e" 50) |
241 eucl_less (infix "<e" 50) |
242 |
242 |
243 lemma One_nonneg: "0 \<le> (\<Sum>Basis::'a::ordered_euclidean_space)" |
243 lemma One_nonneg: "0 \<le> (\<Sum>Basis::'a::ordered_euclidean_space)" |
244 by (auto intro: setsum_nonneg) |
244 by (auto intro: setsum_nonneg) |
245 |
245 |
246 lemma content_closed_interval: |
|
247 fixes a :: "'a::ordered_euclidean_space" |
|
248 assumes "a \<le> b" |
|
249 shows "content {a .. b} = (\<Prod>i\<in>Basis. b\<bullet>i - a\<bullet>i)" |
|
250 using content_cbox[of a b] assms |
|
251 by (simp add: cbox_interval eucl_le[where 'a='a]) |
|
252 |
|
253 lemma integrable_const_ivl[intro]: |
|
254 fixes a::"'a::ordered_euclidean_space" |
|
255 shows "(\<lambda>x. c) integrable_on {a .. b}" |
|
256 unfolding cbox_interval[symmetric] |
|
257 by (rule integrable_const) |
|
258 |
|
259 lemma integrable_on_subinterval: |
|
260 fixes f :: "'n::ordered_euclidean_space \<Rightarrow> 'a::banach" |
|
261 assumes "f integrable_on s" |
|
262 and "{a .. b} \<subseteq> s" |
|
263 shows "f integrable_on {a .. b}" |
|
264 using integrable_on_subcbox[of f s a b] assms |
|
265 by (simp add: cbox_interval) |
|
266 |
|
267 lemma |
246 lemma |
268 fixes a b::"'a::ordered_euclidean_space" |
247 fixes a b::"'a::ordered_euclidean_space" |
269 shows bdd_above_cbox[intro, simp]: "bdd_above (cbox a b)" |
248 shows bdd_above_cbox[intro, simp]: "bdd_above (cbox a b)" |
270 and bdd_below_cbox[intro, simp]: "bdd_below (cbox a b)" |
249 and bdd_below_cbox[intro, simp]: "bdd_below (cbox a b)" |
271 and bdd_above_box[intro, simp]: "bdd_above (box a b)" |
250 and bdd_above_box[intro, simp]: "bdd_above (box a b)" |