equal
deleted
inserted
replaced
39 by (simp add: space_stream_space streams_Stream) |
39 by (simp add: space_stream_space streams_Stream) |
40 |
40 |
41 lemma stream_space_eq_distr: "stream_space M = distr (\<Pi>\<^sub>M i\<in>UNIV. M) (stream_space M) to_stream" |
41 lemma stream_space_eq_distr: "stream_space M = distr (\<Pi>\<^sub>M i\<in>UNIV. M) (stream_space M) to_stream" |
42 unfolding stream_space_def by (rule distr_cong) auto |
42 unfolding stream_space_def by (rule distr_cong) auto |
43 |
43 |
44 lemma sets_stream_space_cong: "sets M = sets N \<Longrightarrow> sets (stream_space M) = sets (stream_space N)" |
44 lemma sets_stream_space_cong[measurable_cong]: |
|
45 "sets M = sets N \<Longrightarrow> sets (stream_space M) = sets (stream_space N)" |
45 using sets_eq_imp_space_eq[of M N] by (simp add: stream_space_def vimage_algebra_def cong: sets_PiM_cong) |
46 using sets_eq_imp_space_eq[of M N] by (simp add: stream_space_def vimage_algebra_def cong: sets_PiM_cong) |
46 |
47 |
47 lemma measurable_snth_PiM: "(\<lambda>\<omega> n. \<omega> !! n) \<in> measurable (stream_space M) (\<Pi>\<^sub>M i\<in>UNIV. M)" |
48 lemma measurable_snth_PiM: "(\<lambda>\<omega> n. \<omega> !! n) \<in> measurable (stream_space M) (\<Pi>\<^sub>M i\<in>UNIV. M)" |
48 by (auto intro!: measurable_vimage_algebra1 |
49 by (auto intro!: measurable_vimage_algebra1 |
49 simp: space_PiM streams_iff_sset sset_range image_subset_iff stream_space_def) |
50 simp: space_PiM streams_iff_sset sset_range image_subset_iff stream_space_def) |