equal
deleted
inserted
replaced
310 note inner = compl(2) and outer = compl(3) |
310 note inner = compl(2) and outer = compl(3) |
311 from compl have [simp]: "B \<in> sets M" by (auto simp: sb borel_eq_closed) |
311 from compl have [simp]: "B \<in> sets M" by (auto simp: sb borel_eq_closed) |
312 case 2 |
312 case 2 |
313 have "M (space M - B) = M (space M) - emeasure M B" by (auto simp: emeasure_compl) |
313 have "M (space M - B) = M (space M) - emeasure M B" by (auto simp: emeasure_compl) |
314 also have "\<dots> = (INF K:{K. K \<subseteq> B \<and> compact K}. M (space M) - M K)" |
314 also have "\<dots> = (INF K:{K. K \<subseteq> B \<and> compact K}. M (space M) - M K)" |
315 unfolding inner by (subst INF_ereal_cminus) force+ |
315 unfolding inner by (subst INF_ereal_minus_right) force+ |
316 also have "\<dots> = (INF U:{U. U \<subseteq> B \<and> compact U}. M (space M - U))" |
316 also have "\<dots> = (INF U:{U. U \<subseteq> B \<and> compact U}. M (space M - U))" |
317 by (rule INF_cong) (auto simp add: emeasure_compl sb compact_imp_closed) |
317 by (rule INF_cong) (auto simp add: emeasure_compl sb compact_imp_closed) |
318 also have "\<dots> \<ge> (INF U:{U. U \<subseteq> B \<and> closed U}. M (space M - U))" |
318 also have "\<dots> \<ge> (INF U:{U. U \<subseteq> B \<and> closed U}. M (space M - U))" |
319 by (rule INF_superset_mono) (auto simp add: compact_imp_closed) |
319 by (rule INF_superset_mono) (auto simp add: compact_imp_closed) |
320 also have "(INF U:{U. U \<subseteq> B \<and> closed U}. M (space M - U)) = |
320 also have "(INF U:{U. U \<subseteq> B \<and> closed U}. M (space M - U)) = |
329 ultimately show ?case by (auto intro!: antisym simp: sets_eq_imp_space_eq[OF sb]) |
329 ultimately show ?case by (auto intro!: antisym simp: sets_eq_imp_space_eq[OF sb]) |
330 |
330 |
331 case 1 |
331 case 1 |
332 have "M (space M - B) = M (space M) - emeasure M B" by (auto simp: emeasure_compl) |
332 have "M (space M - B) = M (space M) - emeasure M B" by (auto simp: emeasure_compl) |
333 also have "\<dots> = (SUP U: {U. B \<subseteq> U \<and> open U}. M (space M) - M U)" |
333 also have "\<dots> = (SUP U: {U. B \<subseteq> U \<and> open U}. M (space M) - M U)" |
334 unfolding outer by (subst SUP_ereal_cminus) auto |
334 unfolding outer by (subst SUP_ereal_minus_right) auto |
335 also have "\<dots> = (SUP U:{U. B \<subseteq> U \<and> open U}. M (space M - U))" |
335 also have "\<dots> = (SUP U:{U. B \<subseteq> U \<and> open U}. M (space M - U))" |
336 by (rule SUP_cong) (auto simp add: emeasure_compl sb compact_imp_closed) |
336 by (rule SUP_cong) (auto simp add: emeasure_compl sb compact_imp_closed) |
337 also have "\<dots> = (SUP K:{K. K \<subseteq> space M - B \<and> closed K}. emeasure M K)" |
337 also have "\<dots> = (SUP K:{K. K \<subseteq> space M - B \<and> closed K}. emeasure M K)" |
338 by (subst SUP_image [of "\<lambda>u. space M - u", symmetric, simplified comp_def]) |
338 by (subst SUP_image [of "\<lambda>u. space M - u", symmetric, simplified comp_def]) |
339 (rule SUP_cong, auto simp: sU) |
339 (rule SUP_cong, auto simp: sU) |