src/HOL/Probability/Measure_Space.thy
changeset 51351 dd1dd470690b
parent 51000 c9adb50f74ad
child 53374 a14d2a854c02
     1.1 --- a/src/HOL/Probability/Measure_Space.thy	Tue Mar 05 15:43:21 2013 +0100
     1.2 +++ b/src/HOL/Probability/Measure_Space.thy	Tue Mar 05 15:43:22 2013 +0100
     1.3 @@ -385,7 +385,7 @@
     1.4      finally have "f (A n - (\<Inter>i. A i)) + f (\<Inter>i. A i) = f (A n)" . }
     1.5    ultimately have "(INF n. f (A n)) = f (\<Inter>i. A i)"
     1.6      by simp
     1.7 -  with LIMSEQ_ereal_INFI[OF decseq_fA]
     1.8 +  with LIMSEQ_INF[OF decseq_fA]
     1.9    show "(\<lambda>i. f (A i)) ----> f (\<Inter>i. A i)" by simp
    1.10  qed
    1.11  
    1.12 @@ -565,7 +565,7 @@
    1.13  lemma Lim_emeasure_decseq:
    1.14    assumes A: "range A \<subseteq> sets M" "decseq A" and fin: "\<And>i. emeasure M (A i) \<noteq> \<infinity>"
    1.15    shows "(\<lambda>i. emeasure M (A i)) ----> emeasure M (\<Inter>i. A i)"
    1.16 -  using LIMSEQ_ereal_INFI[OF decseq_emeasure, OF A]
    1.17 +  using LIMSEQ_INF[OF decseq_emeasure, OF A]
    1.18    using INF_emeasure_decseq[OF A fin] by simp
    1.19  
    1.20  lemma emeasure_subadditive: