equal
deleted
inserted
replaced
161 "f \<in> measurable M (M1 \<Otimes>\<^sub>M M2) \<longleftrightarrow> (fst \<circ> f) \<in> measurable M M1 \<and> (snd \<circ> f) \<in> measurable M M2" |
161 "f \<in> measurable M (M1 \<Otimes>\<^sub>M M2) \<longleftrightarrow> (fst \<circ> f) \<in> measurable M M1 \<and> (snd \<circ> f) \<in> measurable M M2" |
162 by (auto intro: measurable_pair[of f M M1 M2]) |
162 by (auto intro: measurable_pair[of f M M1 M2]) |
163 |
163 |
164 lemma measurable_split_conv: |
164 lemma measurable_split_conv: |
165 "(\<lambda>(x, y). f x y) \<in> measurable A B \<longleftrightarrow> (\<lambda>x. f (fst x) (snd x)) \<in> measurable A B" |
165 "(\<lambda>(x, y). f x y) \<in> measurable A B \<longleftrightarrow> (\<lambda>x. f (fst x) (snd x)) \<in> measurable A B" |
166 by (intro arg_cong2[where f="op \<in>"]) auto |
166 by (intro arg_cong2[where f="(\<in>)"]) auto |
167 |
167 |
168 lemma measurable_pair_swap': "(\<lambda>(x,y). (y, x)) \<in> measurable (M1 \<Otimes>\<^sub>M M2) (M2 \<Otimes>\<^sub>M M1)" |
168 lemma measurable_pair_swap': "(\<lambda>(x,y). (y, x)) \<in> measurable (M1 \<Otimes>\<^sub>M M2) (M2 \<Otimes>\<^sub>M M1)" |
169 by (auto intro!: measurable_Pair simp: measurable_split_conv) |
169 by (auto intro!: measurable_Pair simp: measurable_split_conv) |
170 |
170 |
171 lemma measurable_pair_swap: |
171 lemma measurable_pair_swap: |