src/HOL/Probability/Complete_Measure.thy
changeset 43920 cedb5cb948fd
parent 42866 b0746bd57a41
child 46731 5302e932d1e5
     1.1 --- a/src/HOL/Probability/Complete_Measure.thy	Tue Jul 19 14:35:44 2011 +0200
     1.2 +++ b/src/HOL/Probability/Complete_Measure.thy	Tue Jul 19 14:36:12 2011 +0200
     1.3 @@ -253,7 +253,7 @@
     1.4  qed
     1.5  
     1.6  lemma (in completeable_measure_space) completion_ex_borel_measurable_pos:
     1.7 -  fixes g :: "'a \<Rightarrow> extreal"
     1.8 +  fixes g :: "'a \<Rightarrow> ereal"
     1.9    assumes g: "g \<in> borel_measurable completion" and "\<And>x. 0 \<le> g x"
    1.10    shows "\<exists>g'\<in>borel_measurable M. (AE x. g x = g' x)"
    1.11  proof -
    1.12 @@ -279,7 +279,7 @@
    1.13  qed
    1.14  
    1.15  lemma (in completeable_measure_space) completion_ex_borel_measurable:
    1.16 -  fixes g :: "'a \<Rightarrow> extreal"
    1.17 +  fixes g :: "'a \<Rightarrow> ereal"
    1.18    assumes g: "g \<in> borel_measurable completion"
    1.19    shows "\<exists>g'\<in>borel_measurable M. (AE x. g x = g' x)"
    1.20  proof -