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
```