src/HOL/Analysis/Borel_Space.thy
changeset 67399 eab6ce8368fa
parent 67278 c60e3d615b8c
child 67685 bdff8bf0a75b
     1.1 --- a/src/HOL/Analysis/Borel_Space.thy	Wed Jan 10 15:21:49 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Borel_Space.thy	Wed Jan 10 15:25:09 2018 +0100
     1.3 @@ -110,8 +110,8 @@
     1.4    show "eventually (\<lambda>h. (f (x + h) - f x) / h \<ge> 0) (at 0)"
     1.5    proof (subst eventually_at_topological, intro exI conjI ballI impI)
     1.6      have "open (interior A)" by simp
     1.7 -    hence "open (op + (-x) ` interior A)" by (rule open_translation)
     1.8 -    also have "(op + (-x) ` interior A) = ?A'" by auto
     1.9 +    hence "open ((+) (-x) ` interior A)" by (rule open_translation)
    1.10 +    also have "((+) (-x) ` interior A) = ?A'" by auto
    1.11      finally show "open ?A'" .
    1.12    next
    1.13      from \<open>x \<in> interior A\<close> show "0 \<in> ?A'" by auto
    1.14 @@ -1701,7 +1701,7 @@
    1.15  
    1.16  definition [simp]: "is_borel f M \<longleftrightarrow> f \<in> borel_measurable M"
    1.17  
    1.18 -lemma is_borel_transfer[transfer_rule]: "rel_fun (rel_fun op = pcr_ennreal) op = is_borel is_borel"
    1.19 +lemma is_borel_transfer[transfer_rule]: "rel_fun (rel_fun (=) pcr_ennreal) (=) is_borel is_borel"
    1.20    unfolding is_borel_def[abs_def]
    1.21  proof (safe intro!: rel_funI ext dest!: rel_fun_eq_pcr_ennreal[THEN iffD1])
    1.22    fix f and M :: "'a measure"