diff -r cfe8ee8a1371 -r 382bd3173584 src/HOL/Probability/Borel_Space.thy
--- 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\space M. x \ A} \ sets M \ indicator A \ borel_measurable M"
+ unfolding indicator_def[abs_def]
+ by (auto intro!: measurable_If)
+
lemma borel_measurable_indicator_iff:
"(indicator A :: 'a \ 'x::{t1_space, zero_neq_one}) \ borel_measurable M \ A \ space M \ sets M"
(is "?I \ borel_measurable M \ _")