src/HOL/Probability/Measure_Space.thy
changeset 51000 c9adb50f74ad
parent 50419 3177d0374701
child 51351 dd1dd470690b
     1.1 --- a/src/HOL/Probability/Measure_Space.thy	Thu Jan 31 11:31:27 2013 +0100
     1.2 +++ b/src/HOL/Probability/Measure_Space.thy	Thu Jan 31 11:31:30 2013 +0100
     1.3 @@ -50,7 +50,7 @@
     1.4    then have "\<And>n. (\<Sum>j<n. f j * indicator (A j) x) = (if i < n then f i else 0 :: ereal)"
     1.5      by (auto simp: setsum_cases)
     1.6    moreover have "(SUP n. if i < n then f i else 0) = (f i :: ereal)"
     1.7 -  proof (rule ereal_SUPI)
     1.8 +  proof (rule SUP_eqI)
     1.9      fix y :: ereal assume "\<And>n. n \<in> UNIV \<Longrightarrow> (if i < n then f i else 0) \<le> y"
    1.10      from this[of "Suc i"] show "f i \<le> y" by auto
    1.11    qed (insert assms, simp)
    1.12 @@ -523,7 +523,7 @@
    1.13  lemma SUP_emeasure_incseq:
    1.14    assumes A: "range A \<subseteq> sets M" "incseq A"
    1.15    shows "(SUP n. emeasure M (A n)) = emeasure M (\<Union>i. A i)"
    1.16 -  using LIMSEQ_ereal_SUPR[OF incseq_emeasure, OF A] Lim_emeasure_incseq[OF A]
    1.17 +  using LIMSEQ_SUP[OF incseq_emeasure, OF A] Lim_emeasure_incseq[OF A]
    1.18    by (simp add: LIMSEQ_unique)
    1.19  
    1.20  lemma decseq_emeasure:
    1.21 @@ -1570,7 +1570,7 @@
    1.22        have "incseq (\<lambda>i. ?M (F i))"
    1.23          using `incseq F` unfolding incseq_def by (auto simp: card_mono dest: finite_subset)
    1.24        then have "(\<lambda>i. ?M (F i)) ----> (SUP n. ?M (F n))"
    1.25 -        by (rule LIMSEQ_ereal_SUPR)
    1.26 +        by (rule LIMSEQ_SUP)
    1.27  
    1.28        moreover have "(SUP n. ?M (F n)) = \<infinity>"
    1.29        proof (rule SUP_PInfty)