equal
deleted
inserted
replaced
1003 show "f i \<in> A k i " by (auto simp: `finite I`) |
1003 show "f i \<in> A k i " by (auto simp: `finite I`) |
1004 qed (simp add: `domain f = I` `finite I`) |
1004 qed (simp add: `domain f = I` `finite I`) |
1005 then show "f \<in> (\<Union>n. Pi' I (A n))" by auto |
1005 then show "f \<in> (\<Union>n. Pi' I (A n))" by auto |
1006 qed (auto simp: Pi'_def `finite I`) |
1006 qed (auto simp: Pi'_def `finite I`) |
1007 |
1007 |
1008 text {* adapted from @{thm sigma_prod_algebra_sigma_eq} *} |
1008 text {* adapted from @{thm sets_PiM_sigma} *} |
1009 |
1009 |
1010 lemma sigma_fprod_algebra_sigma_eq: |
1010 lemma sigma_fprod_algebra_sigma_eq: |
1011 fixes E :: "'i \<Rightarrow> 'a set set" and S :: "'i \<Rightarrow> nat \<Rightarrow> 'a set" |
1011 fixes E :: "'i \<Rightarrow> 'a set set" and S :: "'i \<Rightarrow> nat \<Rightarrow> 'a set" |
1012 assumes [simp]: "finite I" "I \<noteq> {}" |
1012 assumes [simp]: "finite I" "I \<noteq> {}" |
1013 and S_union: "\<And>i. i \<in> I \<Longrightarrow> (\<Union>j. S i j) = space (M i)" |
1013 and S_union: "\<And>i. i \<in> I \<Longrightarrow> (\<Union>j. S i j) = space (M i)" |