equal
deleted
inserted
replaced
108 proof (intro exI conjI) |
108 proof (intro exI conjI) |
109 def G \<equiv> "\<lambda>j. (\<Union>i. if j \<in> J i then F i j else X i)" |
109 def G \<equiv> "\<lambda>j. (\<Union>i. if j \<in> J i then F i j else X i)" |
110 show "(\<Union>i. X i) \<in> sets M" "countable (\<Union>i. J i)" "G \<in> (\<Union>i. J i) \<rightarrow> sets M" |
110 show "(\<Union>i. X i) \<in> sets M" "countable (\<Union>i. J i)" "G \<in> (\<Union>i. J i) \<rightarrow> sets M" |
111 using XFJ by (auto simp: G_def Pi_iff) |
111 using XFJ by (auto simp: G_def Pi_iff) |
112 show "UNION UNIV A = (UNIV - (\<Union>i. J i)) \<times> (\<Union>i. X i) \<union> (SIGMA j:\<Union>i. J i. \<Union>i. if j \<in> J i then F i j else X i)" |
112 show "UNION UNIV A = (UNIV - (\<Union>i. J i)) \<times> (\<Union>i. X i) \<union> (SIGMA j:\<Union>i. J i. \<Union>i. if j \<in> J i then F i j else X i)" |
113 unfolding A_eq by (auto split: split_if_asm) |
113 unfolding A_eq by (auto split: if_split_asm) |
114 qed |
114 qed |
115 qed |
115 qed |
116 |
116 |
117 context |
117 context |
118 fixes EXP :: "(real \<Rightarrow> bool) measure" |
118 fixes EXP :: "(real \<Rightarrow> bool) measure" |