summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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