src/HOL/Probability/Borel_Space.thy
changeset 57259 3a448982a74a
parent 57235 b0b9a10e4bf4
child 57275 0ddb5b755cdc
     1.1 --- a/src/HOL/Probability/Borel_Space.thy	Mon Jun 16 16:21:52 2014 +0200
     1.2 +++ b/src/HOL/Probability/Borel_Space.thy	Mon Jun 16 17:52:33 2014 +0200
     1.3 @@ -921,6 +921,15 @@
     1.4  lemma borel_measurable_arctan [measurable]: "arctan \<in> borel_measurable borel"
     1.5    by (intro borel_measurable_continuous_on1 continuous_intros)
     1.6  
     1.7 +lemma borel_measurable_complex_iff:
     1.8 +  "f \<in> borel_measurable M \<longleftrightarrow>
     1.9 +    (\<lambda>x. Re (f x)) \<in> borel_measurable M \<and> (\<lambda>x. Im (f x)) \<in> borel_measurable M"
    1.10 +  apply auto
    1.11 +  apply (subst fun_complex_eq)
    1.12 +  apply (intro borel_measurable_add)
    1.13 +  apply auto
    1.14 +  done
    1.15 +
    1.16  subsection "Borel space on the extended reals"
    1.17  
    1.18  lemma borel_measurable_ereal[measurable (raw)]: