summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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"