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