src/HOL/Probability/Borel_Space.thy
changeset 50001 382bd3173584
parent 49774 dfa8ddb874ce
child 50002 ce0d316b5b44
--- a/src/HOL/Probability/Borel_Space.thy	Fri Nov 02 14:00:39 2012 +0100
+++ b/src/HOL/Probability/Borel_Space.thy	Fri Nov 02 14:00:39 2012 +0100
@@ -91,6 +91,11 @@
   unfolding indicator_def [abs_def] using A
   by (auto intro!: measurable_If_set)
 
+lemma borel_measurable_indicator': 
+  "{x\<in>space M. x \<in> A} \<in> sets M \<Longrightarrow> indicator A \<in> borel_measurable M"
+  unfolding indicator_def[abs_def]
+  by (auto intro!: measurable_If)
+
 lemma borel_measurable_indicator_iff:
   "(indicator A :: 'a \<Rightarrow> 'x::{t1_space, zero_neq_one}) \<in> borel_measurable M \<longleftrightarrow> A \<inter> space M \<in> sets M"
     (is "?I \<in> borel_measurable M \<longleftrightarrow> _")