src/HOL/Analysis/Embed_Measure.thy
changeset 69313 b021008c5397
parent 69260 0a9688695a1b
child 69566 c41954ee87cf
     1.1 --- a/src/HOL/Analysis/Embed_Measure.thy	Sun Nov 18 09:51:41 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Embed_Measure.thy	Sun Nov 18 18:07:51 2018 +0000
     1.3 @@ -401,7 +401,7 @@
     1.4    also have "\<dots> = (SUP i\<in>Y. \<integral>\<^sup>+ x. f i (from_nat_into B (to_nat_on B x)) \<partial>count_space B)"
     1.5      by(simp add: embed_measure_count_space'[symmetric] inj_on_to_nat_on countable nn_integral_embed_measure' measurable_embed_measure1)
     1.6    also have "\<dots> = ?rhs"
     1.7 -    by(intro arg_cong2[where f="SUPREMUM"] ext nn_integral_cong_AE)(simp_all add: AE_count_space countable)
     1.8 +    by(intro arg_cong2[where f = "\<lambda>A f. Sup (f ` A)"] ext nn_integral_cong_AE)(simp_all add: AE_count_space countable)
     1.9    finally show ?thesis .
    1.10  qed
    1.11