src/HOL/Analysis/Measurable.thy
changeset 64320 ba194424b895
parent 64283 979cdfdf7a79
child 66453 cc19f7ca2ed6
     1.1 --- a/src/HOL/Analysis/Measurable.thy	Thu Oct 20 18:41:58 2016 +0200
     1.2 +++ b/src/HOL/Analysis/Measurable.thy	Thu Oct 20 18:41:59 2016 +0200
     1.3 @@ -646,6 +646,14 @@
     1.4    shows "liminf A \<in> sets M"
     1.5  by (subst liminf_SUP_INF, auto)
     1.6  
     1.7 +lemma measurable_case_enat[measurable (raw)]:
     1.8 +  assumes f: "f \<in> M \<rightarrow>\<^sub>M count_space UNIV" and g: "\<And>i. g i \<in> M \<rightarrow>\<^sub>M N" and h: "h \<in> M \<rightarrow>\<^sub>M N"
     1.9 +  shows "(\<lambda>x. case f x of enat i \<Rightarrow> g i x | \<infinity> \<Rightarrow> h x) \<in> M \<rightarrow>\<^sub>M N"
    1.10 +  apply (rule measurable_compose_countable[OF _ f])
    1.11 +  subgoal for i
    1.12 +    by (cases i) (auto intro: g h)
    1.13 +  done
    1.14 +
    1.15  hide_const (open) pred
    1.16  
    1.17  end