src/HOL/Probability/Radon_Nikodym.thy
changeset 44568 e6f291cb5810
parent 43923 ab93d0190a5d
child 44890 22f665a2e91c
     1.1 --- a/src/HOL/Probability/Radon_Nikodym.thy	Sat Aug 27 17:26:14 2011 +0200
     1.2 +++ b/src/HOL/Probability/Radon_Nikodym.thy	Sun Aug 28 09:20:12 2011 -0700
     1.3 @@ -209,7 +209,7 @@
     1.4      from finite_continuity_from_below[OF _ A] `range A \<subseteq> sets M`
     1.5        M'.finite_continuity_from_below[OF _ A]
     1.6      have convergent: "(\<lambda>i. ?d (A i)) ----> ?d (\<Union>i. A i)"
     1.7 -      by (auto intro!: LIMSEQ_diff)
     1.8 +      by (auto intro!: tendsto_diff)
     1.9      obtain n :: nat where "- ?d (\<Union>i. A i) / e < real n" using reals_Archimedean2 by auto
    1.10      moreover from order_trans[OF decseq_le[OF decseq convergent] dA_less]
    1.11      have "real n \<le> - ?d (\<Union>i. A i) / e" using `0<e` by (simp add: field_simps)
    1.12 @@ -295,7 +295,7 @@
    1.13      from
    1.14        finite_continuity_from_above[OF `range A \<subseteq> sets M` A]
    1.15        M'.finite_continuity_from_above[OF `range A \<subseteq> sets M` A]
    1.16 -    have "(\<lambda>i. ?d (A i)) ----> ?d (\<Inter>i. A i)" by (intro LIMSEQ_diff)
    1.17 +    have "(\<lambda>i. ?d (A i)) ----> ?d (\<Inter>i. A i)" by (intro tendsto_diff)
    1.18      thus "?d (space M) \<le> ?d (\<Inter>i. A i)" using mono_dA[THEN monoD, of 0 _]
    1.19        by (rule_tac LIMSEQ_le_const) (auto intro!: exI)
    1.20    next