src/HOL/Probability/Complete_Measure.thy
changeset 41023 9118eb4eb8dc
parent 40871 688f6ff859e1
child 41097 a1abfa4e2b44
     1.1 --- a/src/HOL/Probability/Complete_Measure.thy	Mon Dec 06 19:18:02 2010 +0100
     1.2 +++ b/src/HOL/Probability/Complete_Measure.thy	Fri Dec 03 15:25:14 2010 +0100
     1.3 @@ -243,7 +243,7 @@
     1.4  qed
     1.5  
     1.6  lemma (in completeable_measure_space) completion_ex_borel_measurable:
     1.7 -  fixes g :: "'a \<Rightarrow> pinfreal"
     1.8 +  fixes g :: "'a \<Rightarrow> pextreal"
     1.9    assumes g: "g \<in> borel_measurable completion"
    1.10    shows "\<exists>g'\<in>borel_measurable M. (AE x. g x = g' x)"
    1.11  proof -