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.4  header {*Caratheodory Extension Theorem*}
     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"
    1.20                by (simp add: lambda_system_strong_sum pos A disj eq_fa add_left_mono atLeast0LessThan[symmetric])
    1.21            next