src/HOL/Analysis/Embed_Measure.thy
 changeset 69260 0a9688695a1b parent 69180 922833cc6839 child 69313 b021008c5397
```     1.1 --- a/src/HOL/Analysis/Embed_Measure.thy	Wed Nov 07 23:03:45 2018 +0100
1.2 +++ b/src/HOL/Analysis/Embed_Measure.thy	Thu Nov 08 09:11:52 2018 +0100
1.3 @@ -381,24 +381,24 @@
1.4    assumes nonempty: "Y \<noteq> {}"
1.5    and chain: "Complete_Partial_Order.chain (\<le>) (f ` Y)"
1.6    and countable: "countable B"
1.7 -  shows "(\<integral>\<^sup>+ x. (SUP i:Y. f i x) \<partial>count_space B) = (SUP i:Y. (\<integral>\<^sup>+ x. f i x \<partial>count_space B))"
1.8 +  shows "(\<integral>\<^sup>+ x. (SUP i\<in>Y. f i x) \<partial>count_space B) = (SUP i\<in>Y. (\<integral>\<^sup>+ x. f i x \<partial>count_space B))"
1.9    (is "?lhs = ?rhs")
1.10  proof -
1.11    let ?f = "(\<lambda>i x. f i (from_nat_into B x) * indicator (to_nat_on B ` B) x)"
1.12 -  have "?lhs = \<integral>\<^sup>+ x. (SUP i:Y. f i (from_nat_into B (to_nat_on B x))) \<partial>count_space B"
1.13 +  have "?lhs = \<integral>\<^sup>+ x. (SUP i\<in>Y. f i (from_nat_into B (to_nat_on B x))) \<partial>count_space B"
1.15 -  also have "\<dots> = \<integral>\<^sup>+ x. (SUP i:Y. f i (from_nat_into B x)) \<partial>count_space (to_nat_on B ` B)"
1.16 +  also have "\<dots> = \<integral>\<^sup>+ x. (SUP i\<in>Y. f i (from_nat_into B x)) \<partial>count_space (to_nat_on B ` B)"
1.17      by(simp add: embed_measure_count_space'[symmetric] inj_on_to_nat_on countable nn_integral_embed_measure' measurable_embed_measure1)
1.18 -  also have "\<dots> = \<integral>\<^sup>+ x. (SUP i:Y. ?f i x) \<partial>count_space UNIV"
1.19 +  also have "\<dots> = \<integral>\<^sup>+ x. (SUP i\<in>Y. ?f i x) \<partial>count_space UNIV"
1.20      by(simp add: nn_integral_count_space_indicator ennreal_indicator[symmetric] SUP_mult_right_ennreal nonempty)
1.21 -  also have "\<dots> = (SUP i:Y. \<integral>\<^sup>+ x. ?f i x \<partial>count_space UNIV)"
1.22 +  also have "\<dots> = (SUP i\<in>Y. \<integral>\<^sup>+ x. ?f i x \<partial>count_space UNIV)"
1.23    proof(rule nn_integral_monotone_convergence_SUP_nat)
1.24      show "Complete_Partial_Order.chain (\<le>) (?f ` Y)"
1.25        by(rule chain_imageI[OF chain, unfolded image_image])(auto intro!: le_funI split: split_indicator dest: le_funD)
1.26    qed fact
1.27 -  also have "\<dots> = (SUP i:Y. \<integral>\<^sup>+ x. f i (from_nat_into B x) \<partial>count_space (to_nat_on B ` B))"
1.28 +  also have "\<dots> = (SUP i\<in>Y. \<integral>\<^sup>+ x. f i (from_nat_into B x) \<partial>count_space (to_nat_on B ` B))"