--- a/src/HOL/Probability/Sigma_Algebra.thy Mon Nov 24 12:20:35 2014 +0100
+++ b/src/HOL/Probability/Sigma_Algebra.thy Mon Nov 24 12:20:14 2014 +0100
@@ -1933,12 +1933,6 @@
f \<in> measurable M M' \<longleftrightarrow> g \<in> measurable N N'"
by (metis measurable_cong)
-lemma measurable_eqI:
- "\<lbrakk> space m1 = space m1' ; space m2 = space m2' ;
- sets m1 = sets m1' ; sets m2 = sets m2' \<rbrakk>
- \<Longrightarrow> measurable m1 m2 = measurable m1' m2'"
- by (simp add: measurable_def sigma_algebra_iff2)
-
lemma measurable_compose:
assumes f: "f \<in> measurable M N" and g: "g \<in> measurable N L"
shows "(\<lambda>x. g (f x)) \<in> measurable M L"
@@ -1990,6 +1984,9 @@
lemma measurable_ident: "id \<in> measurable M M"
by (auto simp add: measurable_def)
+lemma measurable_id: "(\<lambda>x. x) \<in> measurable M M"
+ by (simp add: measurable_def)
+
lemma measurable_ident_sets:
assumes eq: "sets M = sets M'" shows "(\<lambda>x. x) \<in> measurable M M'"
using measurable_ident[of M]