src/HOL/Multivariate_Analysis/Integration.thy
changeset 38656 d5d342611edb
parent 37665 579258a77fec
child 39302 d7728f65b353
     1.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Mon Aug 23 17:46:13 2010 +0200
     1.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Mon Aug 23 19:35:57 2010 +0200
     1.3 @@ -5287,10 +5287,10 @@
     1.4      qed finally show ?case . qed qed
     1.5  
     1.6  lemma nonnegative_absolutely_integrable: fixes f::"'n::ordered_euclidean_space \<Rightarrow> 'm::ordered_euclidean_space"
     1.7 -  assumes "\<forall>x\<in>s. \<forall>i. 0 \<le> f(x)$$i" "f integrable_on s"
     1.8 +  assumes "\<forall>x\<in>s. \<forall>i<DIM('m). 0 \<le> f(x)$$i" "f integrable_on s"
     1.9    shows "f absolutely_integrable_on s"
    1.10    unfolding absolutely_integrable_abs_eq apply rule defer
    1.11 -  apply(rule integrable_eq[of _ f]) using assms by auto
    1.12 +  apply(rule integrable_eq[of _ f]) using assms apply-apply(subst euclidean_eq) by auto
    1.13  
    1.14  lemma absolutely_integrable_integrable_bound: fixes f::"'n::ordered_euclidean_space \<Rightarrow> 'm::ordered_euclidean_space"
    1.15    assumes "\<forall>x\<in>s. norm(f x) \<le> g x" "f integrable_on s" "g integrable_on s"