src/HOL/Analysis/Ordered_Euclidean_Space.thy
changeset 63886 685fb01256af
parent 63627 6ddb43c6b711
child 64267 b9a1486e79be
     1.1 --- a/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Thu Sep 15 22:41:05 2016 +0200
     1.2 +++ b/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Fri Sep 16 13:56:51 2016 +0200
     1.3 @@ -243,27 +243,6 @@
     1.4  lemma One_nonneg: "0 \<le> (\<Sum>Basis::'a::ordered_euclidean_space)"
     1.5    by (auto intro: setsum_nonneg)
     1.6  
     1.7 -lemma content_closed_interval:
     1.8 -  fixes a :: "'a::ordered_euclidean_space"
     1.9 -  assumes "a \<le> b"
    1.10 -  shows "content {a .. b} = (\<Prod>i\<in>Basis. b\<bullet>i - a\<bullet>i)"
    1.11 -  using content_cbox[of a b] assms
    1.12 -  by (simp add: cbox_interval eucl_le[where 'a='a])
    1.13 -
    1.14 -lemma integrable_const_ivl[intro]:
    1.15 -  fixes a::"'a::ordered_euclidean_space"
    1.16 -  shows "(\<lambda>x. c) integrable_on {a .. b}"
    1.17 -  unfolding cbox_interval[symmetric]
    1.18 -  by (rule integrable_const)
    1.19 -
    1.20 -lemma integrable_on_subinterval:
    1.21 -  fixes f :: "'n::ordered_euclidean_space \<Rightarrow> 'a::banach"
    1.22 -  assumes "f integrable_on s"
    1.23 -    and "{a .. b} \<subseteq> s"
    1.24 -  shows "f integrable_on {a .. b}"
    1.25 -  using integrable_on_subcbox[of f s a b] assms
    1.26 -  by (simp add: cbox_interval)
    1.27 -
    1.28  lemma
    1.29    fixes a b::"'a::ordered_euclidean_space"
    1.30    shows bdd_above_cbox[intro, simp]: "bdd_above (cbox a b)"