src/HOL/Probability/Probability_Measure.thy
changeset 56166 9a241bc276cd
parent 54418 3b8e33d1a39a
child 56993 e5366291d6aa
     1.1 --- a/src/HOL/Probability/Probability_Measure.thy	Sat Mar 15 16:54:32 2014 +0100
     1.2 +++ b/src/HOL/Probability/Probability_Measure.thy	Sun Mar 16 18:09:04 2014 +0100
     1.3 @@ -159,7 +159,7 @@
     1.4    moreover
     1.5    { fix y assume y: "y \<in> I"
     1.6      with q(2) `open I` have "Sup ((\<lambda>x. q x + ?F x * (y - x)) ` I) = q y"
     1.7 -      by (auto intro!: cSup_eq_maximum convex_le_Inf_differential image_eqI[OF _ y] simp: interior_open) }
     1.8 +      by (auto intro!: cSup_eq_maximum convex_le_Inf_differential image_eqI [OF _ y] simp: interior_open simp del: Sup_image_eq Inf_image_eq) }
     1.9    ultimately have "q (expectation X) = Sup ((\<lambda>x. q x + ?F x * (expectation X - x)) ` I)"
    1.10      by simp
    1.11    also have "\<dots> \<le> expectation (\<lambda>w. q (X w))"