src/HOL/Probability/Stream_Space.thy
changeset 64320 ba194424b895
parent 64008 17a20ca86d62
child 66453 cc19f7ca2ed6
     1.1 --- a/src/HOL/Probability/Stream_Space.thy	Thu Oct 20 18:41:58 2016 +0200
     1.2 +++ b/src/HOL/Probability/Stream_Space.thy	Thu Oct 20 18:41:59 2016 +0200
     1.3 @@ -446,6 +446,17 @@
     1.4      by (cases "xs = []") (auto simp: * space_stream_space del: in_listsD)
     1.5  qed (auto simp: * ae sets_M del: in_listsD intro!: streams_sets)
     1.6  
     1.7 +lemma sets_sstart[measurable]: "sstart \<Omega> xs \<in> sets (stream_space (count_space UNIV))"
     1.8 +proof (induction xs)
     1.9 +  case (Cons x xs)
    1.10 +  note this[measurable]
    1.11 +  have "sstart \<Omega> (x # xs) = {\<omega>\<in>space (stream_space (count_space UNIV)). \<omega> \<in> sstart \<Omega> (x # xs)}"
    1.12 +    by (auto simp: space_stream_space)
    1.13 +  also have "\<dots> \<in> sets (stream_space (count_space UNIV))"
    1.14 +    unfolding in_sstart by measurable
    1.15 +  finally show ?case .
    1.16 +qed (auto intro!: streams_sets)
    1.17 +
    1.18  primrec scylinder :: "'a set \<Rightarrow> 'a set list \<Rightarrow> 'a stream set"
    1.19  where
    1.20    "scylinder S [] = streams S"