src/HOL/Probability/Caratheodory.thy
changeset 40859 de0b30e6c2d2
parent 39096 111756225292
child 41023 9118eb4eb8dc
     1.1 --- a/src/HOL/Probability/Caratheodory.thy	Wed Dec 01 06:50:54 2010 -0800
     1.2 +++ b/src/HOL/Probability/Caratheodory.thy	Wed Dec 01 19:20:30 2010 +0100
     1.3 @@ -760,7 +760,7 @@
     1.4  
     1.5  theorem (in algebra) caratheodory:
     1.6    assumes posf: "positive f" and ca: "countably_additive M f"
     1.7 -  shows "\<exists>\<mu> :: 'a set \<Rightarrow> pinfreal. (\<forall>s \<in> sets M. \<mu> s = f s) \<and> measure_space (sigma (space M) (sets M)) \<mu>"
     1.8 +  shows "\<exists>\<mu> :: 'a set \<Rightarrow> pinfreal. (\<forall>s \<in> sets M. \<mu> s = f s) \<and> measure_space (sigma M) \<mu>"
     1.9    proof -
    1.10      have inc: "increasing M f"
    1.11        by (metis additive_increasing ca countably_additive_additive posf)
    1.12 @@ -778,7 +778,7 @@
    1.13      hence sgs_sb: "sigma_sets (space M) (sets M) \<subseteq> ls"
    1.14        using sigma_algebra.sigma_sets_subset [OF sls, of "sets M"]
    1.15        by simp
    1.16 -    have "measure_space (sigma (space M) (sets M)) ?infm"
    1.17 +    have "measure_space (sigma M) ?infm"
    1.18        unfolding sigma_def
    1.19        by (rule measure_down [OF mls], rule sigma_algebra_sigma_sets)
    1.20           (simp_all add: sgs_sb space_closed)