src/HOL/Probability/Caratheodory.thy
 changeset 44106 0e018cbcc0de parent 43920 cedb5cb948fd child 44568 e6f291cb5810
```     1.1 --- a/src/HOL/Probability/Caratheodory.thy	Tue Aug 09 18:52:18 2011 +0200
1.2 +++ b/src/HOL/Probability/Caratheodory.thy	Tue Aug 09 20:24:48 2011 +0200
1.3 @@ -6,7 +6,7 @@
1.5
1.6  theory Caratheodory
1.7 -  imports Sigma_Algebra Extended_Real_Limits
1.8 +imports Sigma_Algebra "~~/src/HOL/Multivariate_Analysis/Extended_Real_Limits"
1.9  begin
1.10
1.11  lemma sums_def2:
1.12 @@ -433,8 +433,7 @@
1.13              hence eq_fa: "f a = f (a \<inter> (\<Union>i\<in>{0..<n}. A i)) + f (a - (\<Union>i\<in>{0..<n}. A i))"
1.14                by (simp add: lambda_system_eq UNION_in)
1.15              have "f (a - (\<Union>i. A i)) \<le> f (a - (\<Union>i\<in>{0..<n}. A i))"
1.16 -              by (blast intro: increasingD [OF inc] UNION_eq_Union_image
1.17 -                               UNION_in U_in)
1.18 +              by (blast intro: increasingD [OF inc] UNION_in U_in)
1.19              thus "(\<Sum>i<n. f (a \<inter> A i)) + f (a - (\<Union>i. A i)) \<le> f a"