src/HOL/Probability/Lebesgue_Measure.thy
changeset 54257 5c7a3b6b05a9
parent 53374 a14d2a854c02
child 54775 2d3df8633dad
     1.1 --- a/src/HOL/Probability/Lebesgue_Measure.thy	Tue Nov 05 05:48:08 2013 +0100
     1.2 +++ b/src/HOL/Probability/Lebesgue_Measure.thy	Tue Nov 05 09:44:57 2013 +0100
     1.3 @@ -1138,7 +1138,7 @@
     1.4      show "\<And>i x. 0 \<le> ?f i x"
     1.5        using nonneg by (auto split: split_indicator)
     1.6    qed
     1.7 -  also have "\<dots> = (SUP i::nat. F (a + real i) - F a)"
     1.8 +  also have "\<dots> = (SUP i::nat. ereal (F (a + real i) - F a))"
     1.9      by (subst positive_integral_FTC_atLeastAtMost[OF f_borel f nonneg]) auto
    1.10    also have "\<dots> = T - F a"
    1.11    proof (rule SUP_Lim_ereal)