src/HOL/Analysis/Borel_Space.thy
changeset 67278 c60e3d615b8c
parent 66164 2d79288b042c
child 67399 eab6ce8368fa
     1.1 --- a/src/HOL/Analysis/Borel_Space.thy	Sun Dec 24 14:46:26 2017 +0100
     1.2 +++ b/src/HOL/Analysis/Borel_Space.thy	Sun Dec 24 14:28:10 2017 +0100
     1.3 @@ -1515,6 +1515,11 @@
     1.4    apply auto
     1.5    done
     1.6  
     1.7 +lemma powr_real_measurable [measurable]:
     1.8 +  assumes "f \<in> measurable M borel" "g \<in> measurable M borel"
     1.9 +  shows   "(\<lambda>x. f x powr g x :: real) \<in> measurable M borel"
    1.10 +  using assms by (simp_all add: powr_def)
    1.11 +
    1.12  lemma measurable_of_bool[measurable]: "of_bool \<in> count_space UNIV \<rightarrow>\<^sub>M borel"
    1.13    by simp
    1.14