src/HOL/Analysis/Measure_Space.thy
changeset 67399 eab6ce8368fa
parent 66453 cc19f7ca2ed6
child 67673 c8caefb20564
     1.1 --- a/src/HOL/Analysis/Measure_Space.thy	Wed Jan 10 15:21:49 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Measure_Space.thy	Wed Jan 10 15:25:09 2018 +0100
     1.3 @@ -2348,7 +2348,7 @@
     1.4    case True
     1.5    show ?thesis
     1.6    proof (rule emeasure_measure_of[OF restrict_space_def])
     1.7 -    show "op \<inter> \<Omega> ` sets M \<subseteq> Pow (\<Omega> \<inter> space M)" "A \<in> sets (restrict_space M \<Omega>)"
     1.8 +    show "(\<inter>) \<Omega> ` sets M \<subseteq> Pow (\<Omega> \<inter> space M)" "A \<in> sets (restrict_space M \<Omega>)"
     1.9        using \<open>A \<subseteq> \<Omega>\<close> \<open>A \<in> sets M\<close> sets.space_closed by (auto simp: sets_restrict_space)
    1.10      show "positive (sets (restrict_space M \<Omega>)) (emeasure M)"
    1.11        by (auto simp: positive_def)
    1.12 @@ -2427,7 +2427,7 @@
    1.13    from sigma_finite_countable obtain C
    1.14      where C: "countable C" "C \<subseteq> sets M" "(\<Union>C) = space M" "\<forall>a\<in>C. emeasure M a \<noteq> \<infinity>"
    1.15      by blast
    1.16 -  let ?C = "op \<inter> A ` C"
    1.17 +  let ?C = "(\<inter>) A ` C"
    1.18    from C have "countable ?C" "?C \<subseteq> sets (restrict_space M A)" "(\<Union>?C) = space (restrict_space M A)"
    1.19      by(auto simp add: sets_restrict_space space_restrict_space)
    1.20    moreover {
    1.21 @@ -2861,7 +2861,7 @@
    1.22        also have "\<dots> = ?S (\<Union>i. X i)"
    1.23          unfolding UN_extend_simps(4)
    1.24          by (auto simp add: suminf_add[symmetric] Diff_eq[symmetric] simp del: UN_simps
    1.25 -                 intro!: SUP_cong arg_cong2[where f="op +"] suminf_emeasure
    1.26 +                 intro!: SUP_cong arg_cong2[where f="(+)"] suminf_emeasure
    1.27                           disjoint_family_on_bisimulation[OF \<open>disjoint_family X\<close>])
    1.28        finally show "(\<Sum>i. ?S (X i)) = ?S (\<Union>i. X i)" .
    1.29      qed
    1.30 @@ -3395,13 +3395,13 @@
    1.31  
    1.32  lemma emeasure_SUP_chain:
    1.33    assumes sets: "\<And>i. i \<in> A \<Longrightarrow> sets (M i) = sets N" "X \<in> sets N"
    1.34 -  assumes ch: "Complete_Partial_Order.chain op \<le> (M ` A)" and "A \<noteq> {}"
    1.35 +  assumes ch: "Complete_Partial_Order.chain (\<le>) (M ` A)" and "A \<noteq> {}"
    1.36    shows "emeasure (SUP i:A. M i) X = (SUP i:A. emeasure (M i) X)"
    1.37  proof (subst emeasure_SUP[OF sets \<open>A \<noteq> {}\<close>])
    1.38    show "(SUP J:{J. J \<noteq> {} \<and> finite J \<and> J \<subseteq> A}. emeasure (SUPREMUM J M) X) = (SUP i:A. emeasure (M i) X)"
    1.39    proof (rule SUP_eq)
    1.40      fix J assume "J \<in> {J. J \<noteq> {} \<and> finite J \<and> J \<subseteq> A}"
    1.41 -    then have J: "Complete_Partial_Order.chain op \<le> (M ` J)" "finite J" "J \<noteq> {}" and "J \<subseteq> A"
    1.42 +    then have J: "Complete_Partial_Order.chain (\<le>) (M ` J)" "finite J" "J \<noteq> {}" and "J \<subseteq> A"
    1.43        using ch[THEN chain_subset, of "M`J"] by auto
    1.44      with in_chain_finite[OF J(1)] obtain j where "j \<in> J" "(SUP j:J. M j) = M j"
    1.45        by auto