equal
deleted
inserted
replaced
540 apply (auto simp: negligible_imp_measurable negligible_Int negligible_imp_measure0 zero_less_measure_iff) |
540 apply (auto simp: negligible_imp_measurable negligible_Int negligible_imp_measure0 zero_less_measure_iff) |
541 done |
541 done |
542 next |
542 next |
543 assume R [rule_format]: "\<forall>x \<in> S. \<forall>e > 0. ?Q x e" |
543 assume R [rule_format]: "\<forall>x \<in> S. \<forall>e > 0. ?Q x e" |
544 let ?\<mu> = "measure lebesgue" |
544 let ?\<mu> = "measure lebesgue" |
545 have "\<exists>U. openin (subtopology euclidean S) U \<and> z \<in> U \<and> negligible U" |
545 have "\<exists>U. openin (top_of_set S) U \<and> z \<in> U \<and> negligible U" |
546 if "z \<in> S" for z |
546 if "z \<in> S" for z |
547 proof (intro exI conjI) |
547 proof (intro exI conjI) |
548 show "openin (subtopology euclidean S) (S \<inter> ball z 1)" |
548 show "openin (top_of_set S) (S \<inter> ball z 1)" |
549 by (simp add: openin_open_Int) |
549 by (simp add: openin_open_Int) |
550 show "z \<in> S \<inter> ball z 1" |
550 show "z \<in> S \<inter> ball z 1" |
551 using \<open>z \<in> S\<close> by auto |
551 using \<open>z \<in> S\<close> by auto |
552 show "negligible (S \<inter> ball z 1)" |
552 show "negligible (S \<inter> ball z 1)" |
553 proof (clarsimp simp: negligible_outer_le) |
553 proof (clarsimp simp: negligible_outer_le) |