src/HOL/Probability/Radon_Nikodym.thy
changeset 43556 0d78c8d31d0d
parent 43340 60e181c4eae4
child 43920 cedb5cb948fd
     1.1 --- a/src/HOL/Probability/Radon_Nikodym.thy	Sun Jun 26 19:10:03 2011 +0200
     1.2 +++ b/src/HOL/Probability/Radon_Nikodym.thy	Mon Jun 27 09:42:46 2011 +0200
     1.3 @@ -314,10 +314,6 @@
     1.4    qed
     1.5  qed
     1.6  
     1.7 -lemma (in finite_measure) real_measure:
     1.8 -  assumes A: "A \<in> sets M" shows "\<exists>r. 0 \<le> r \<and> \<mu> A = extreal r"
     1.9 -  using finite_measure[OF A] positive_measure[OF A] by (cases "\<mu> A") auto
    1.10 -
    1.11  lemma (in finite_measure) Radon_Nikodym_finite_measure:
    1.12    assumes "finite_measure (M\<lparr> measure := \<nu>\<rparr>)" (is "finite_measure ?M'")
    1.13    assumes "absolutely_continuous \<nu>"