src/HOL/Analysis/Embed_Measure.thy
changeset 67399 eab6ce8368fa
parent 67241 73635a5bfa5c
child 69180 922833cc6839
     1.1 --- a/src/HOL/Analysis/Embed_Measure.thy	Wed Jan 10 15:21:49 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Embed_Measure.thy	Wed Jan 10 15:25:09 2018 +0100
     1.3 @@ -159,15 +159,15 @@
     1.4    from assms(1) interpret sigma_finite_measure M .
     1.5    from sigma_finite_countable obtain A where
     1.6        A_props: "countable A" "A \<subseteq> sets M" "\<Union>A = space M" "\<And>X. X\<in>A \<Longrightarrow> emeasure M X \<noteq> \<infinity>" by blast
     1.7 -  from A_props have "countable (op ` f`A)" by auto
     1.8 +  from A_props have "countable ((`) f`A)" by auto
     1.9    moreover
    1.10 -  from inj and A_props have "op ` f`A \<subseteq> sets (embed_measure M f)"
    1.11 +  from inj and A_props have "(`) f`A \<subseteq> sets (embed_measure M f)"
    1.12      by (auto simp: sets_embed_measure)
    1.13    moreover
    1.14 -  from A_props and inj have "\<Union>(op ` f`A) = space (embed_measure M f)"
    1.15 +  from A_props and inj have "\<Union>((`) f`A) = space (embed_measure M f)"
    1.16      by (auto simp: space_embed_measure intro!: imageI)
    1.17    moreover
    1.18 -  from A_props and inj have "\<forall>a\<in>op ` f ` A. emeasure (embed_measure M f) a \<noteq> \<infinity>"
    1.19 +  from A_props and inj have "\<forall>a\<in>(`) f ` A. emeasure (embed_measure M f) a \<noteq> \<infinity>"
    1.20      by (intro ballI, subst emeasure_embed_measure)
    1.21         (auto simp: inj_vimage_image_eq intro: in_sets_embed_measure)
    1.22    ultimately show ?thesis by - (standard, blast)
    1.23 @@ -189,7 +189,7 @@
    1.24    by(rule embed_measure_count_space')(erule subset_inj_on, simp)
    1.25  
    1.26  lemma sets_embed_measure_alt:
    1.27 -    "inj f \<Longrightarrow> sets (embed_measure M f) = (op` f) ` sets M"
    1.28 +    "inj f \<Longrightarrow> sets (embed_measure M f) = ((`) f) ` sets M"
    1.29    by (auto simp: sets_embed_measure)
    1.30  
    1.31  lemma emeasure_embed_measure_image':
    1.32 @@ -210,7 +210,7 @@
    1.33    assumes "inj f"
    1.34    shows "embed_measure A f = embed_measure B f \<longleftrightarrow> A = B" (is "?M = ?N \<longleftrightarrow> _")
    1.35  proof
    1.36 -  from assms have I: "inj (op` f)" by (auto intro: injI dest: injD)
    1.37 +  from assms have I: "inj ((`) f)" by (auto intro: injI dest: injD)
    1.38    assume asm: "?M = ?N"
    1.39    hence "sets (embed_measure A f) = sets (embed_measure B f)" by simp
    1.40    with assms have "sets A = sets B" by (simp only: I inj_image_eq_iff sets_embed_measure_alt)
    1.41 @@ -369,7 +369,7 @@
    1.42  lemma nn_integral_monotone_convergence_SUP_countable:
    1.43    fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> ennreal"
    1.44    assumes nonempty: "Y \<noteq> {}"
    1.45 -  and chain: "Complete_Partial_Order.chain op \<le> (f ` Y)"
    1.46 +  and chain: "Complete_Partial_Order.chain (\<le>) (f ` Y)"
    1.47    and countable: "countable B"
    1.48    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.49    (is "?lhs = ?rhs")
    1.50 @@ -383,7 +383,7 @@
    1.51      by(simp add: nn_integral_count_space_indicator ennreal_indicator[symmetric] SUP_mult_right_ennreal nonempty)
    1.52    also have "\<dots> = (SUP i:Y. \<integral>\<^sup>+ x. ?f i x \<partial>count_space UNIV)"
    1.53    proof(rule nn_integral_monotone_convergence_SUP_nat)
    1.54 -    show "Complete_Partial_Order.chain op \<le> (?f ` Y)"
    1.55 +    show "Complete_Partial_Order.chain (\<le>) (?f ` Y)"
    1.56        by(rule chain_imageI[OF chain, unfolded image_image])(auto intro!: le_funI split: split_indicator dest: le_funD)
    1.57    qed fact
    1.58    also have "\<dots> = (SUP i:Y. \<integral>\<^sup>+ x. f i (from_nat_into B x) \<partial>count_space (to_nat_on B ` B))"