src/HOL/Probability/Lebesgue_Integration.thy
changeset 56166 9a241bc276cd
parent 56154 f0a927235162
child 56193 c726ecfb22b6
     1.1 --- a/src/HOL/Probability/Lebesgue_Integration.thy	Sat Mar 15 16:54:32 2014 +0100
     1.2 +++ b/src/HOL/Probability/Lebesgue_Integration.thy	Sun Mar 16 18:09:04 2014 +0100
     1.3 @@ -936,7 +936,7 @@
     1.4            by (intro ereal_mult_strict_right_mono) (auto simp: image_iff)
     1.5          also have "\<dots> \<le> (SUP i. f i x)" using u(2) by (auto simp: le_fun_def)
     1.6          finally obtain i where "a * u x < f i x" unfolding SUP_def
     1.7 -          by (auto simp add: less_Sup_iff)
     1.8 +          by (auto simp add: less_SUP_iff)
     1.9          hence "a * u x \<le> f i x" by auto
    1.10          thus ?thesis using `x \<in> space M` by auto
    1.11        qed