equal
deleted
inserted
replaced
176 translations |
176 translations |
177 "PIM x:I. M" == "CONST PiM I (%x. M)" |
177 "PIM x:I. M" == "CONST PiM I (%x. M)" |
178 |
178 |
179 lemma prod_algebra_sets_into_space: |
179 lemma prod_algebra_sets_into_space: |
180 "prod_algebra I M \<subseteq> Pow (\<Pi>\<^isub>E i\<in>I. space (M i))" |
180 "prod_algebra I M \<subseteq> Pow (\<Pi>\<^isub>E i\<in>I. space (M i))" |
181 using assms by (auto simp: prod_emb_def prod_algebra_def) |
181 by (auto simp: prod_emb_def prod_algebra_def) |
182 |
182 |
183 lemma prod_algebra_eq_finite: |
183 lemma prod_algebra_eq_finite: |
184 assumes I: "finite I" |
184 assumes I: "finite I" |
185 shows "prod_algebra I M = {(\<Pi>\<^isub>E i\<in>I. X i) |X. X \<in> (\<Pi> j\<in>I. sets (M j))}" (is "?L = ?R") |
185 shows "prod_algebra I M = {(\<Pi>\<^isub>E i\<in>I. X i) |X. X \<in> (\<Pi> j\<in>I. sets (M j))}" (is "?L = ?R") |
186 proof (intro iffI set_eqI) |
186 proof (intro iffI set_eqI) |