src/HOL/Analysis/Borel_Space.thy
changeset 64911 f0e07600de47
parent 64320 ba194424b895
child 66164 2d79288b042c
     1.1 --- a/src/HOL/Analysis/Borel_Space.thy	Tue Jan 17 11:26:21 2017 +0100
     1.2 +++ b/src/HOL/Analysis/Borel_Space.thy	Tue Jan 17 13:59:10 2017 +0100
     1.3 @@ -2126,7 +2126,7 @@
     1.4    shows "(\<lambda>x. \<bar>f x\<bar> powr p) \<in> borel_measurable M"
     1.5  unfolding powr_def by auto
     1.6  
     1.7 -text {* The next one is a variation around \verb+measurable_restrict_space+.*}
     1.8 +text \<open>The next one is a variation around \verb+measurable_restrict_space+.\<close>
     1.9  
    1.10  lemma measurable_restrict_space3:
    1.11    assumes "f \<in> measurable M N" and
    1.12 @@ -2138,7 +2138,7 @@
    1.13        measurable_restrict_space2[of f, of "restrict_space M A", of B, of N] assms(2) space_restrict_space)
    1.14  qed
    1.15  
    1.16 -text {* The next one is a variation around \verb+measurable_piecewise_restrict+.*}
    1.17 +text \<open>The next one is a variation around \verb+measurable_piecewise_restrict+.\<close>
    1.18  
    1.19  lemma measurable_piecewise_restrict2:
    1.20    assumes [measurable]: "\<And>n. A n \<in> sets M"
    1.21 @@ -2162,8 +2162,8 @@
    1.22    fix x assume "x \<in> space M"
    1.23    then obtain n where "x \<in> A n" using assms(2) by blast
    1.24    obtain h where [measurable]: "h \<in> measurable M N" and "\<forall>x \<in> A n. f x = h x" using assms(3) by blast
    1.25 -  then have "f x = h x" using `x \<in> A n` by blast
    1.26 -  moreover have "h x \<in> space N" by (metis measurable_space `x \<in> space M` `h \<in> measurable M N`)
    1.27 +  then have "f x = h x" using \<open>x \<in> A n\<close> by blast
    1.28 +  moreover have "h x \<in> space N" by (metis measurable_space \<open>x \<in> space M\<close> \<open>h \<in> measurable M N\<close>)
    1.29    ultimately show "f x \<in> space N" by simp
    1.30  qed
    1.31