equal
deleted
inserted
replaced
1194 measurable_component_singleton[of True UNIV "case_bool M1 M2"] |
1194 measurable_component_singleton[of True UNIV "case_bool M1 M2"] |
1195 measurable_component_singleton[of False UNIV "case_bool M1 M2"] |
1195 measurable_component_singleton[of False UNIV "case_bool M1 M2"] |
1196 by (subst emeasure_distr) (auto simp: measurable_pair_iff) |
1196 by (subst emeasure_distr) (auto simp: measurable_pair_iff) |
1197 qed simp |
1197 qed simp |
1198 |
1198 |
|
1199 lemma infprod_in_sets[intro]: |
|
1200 fixes E :: "nat \<Rightarrow> 'a set" assumes E: "\<And>i. E i \<in> sets (M i)" |
|
1201 shows "Pi UNIV E \<in> sets (\<Pi>\<^sub>M i\<in>UNIV::nat set. M i)" |
|
1202 proof - |
|
1203 have "Pi UNIV E = (\<Inter>i. prod_emb UNIV M {..i} (\<Pi>\<^sub>E j\<in>{..i}. E j))" |
|
1204 using E E[THEN sets.sets_into_space] |
|
1205 by (auto simp: prod_emb_def Pi_iff extensional_def) |
|
1206 with E show ?thesis by auto |
|
1207 qed |
|
1208 |
1199 end |
1209 end |