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"
```