changeset 41545 | 9c869baf1c66 |
parent 41097 | a1abfa4e2b44 |
child 41830 | 719b0a517c33 |
--- a/src/HOL/Probability/Borel_Space.thy Fri Jan 14 14:21:48 2011 +0100 +++ b/src/HOL/Probability/Borel_Space.thy Fri Jan 14 15:56:42 2011 +0100 @@ -170,7 +170,7 @@ qed lemma (in sigma_algebra) borel_measurable_subalgebra: - assumes "N \<subseteq> sets M" "f \<in> borel_measurable (M\<lparr>sets:=N\<rparr>)" + assumes "sets N \<subseteq> sets M" "space N = space M" "f \<in> borel_measurable N" shows "f \<in> borel_measurable M" using assms unfolding measurable_def by auto