equal
deleted
inserted
replaced
534 proof - |
534 proof - |
535 have "A \<subseteq> (\<Union>i. {from_nat_into A i})" using from_nat_into_surj assms by force |
535 have "A \<subseteq> (\<Union>i. {from_nat_into A i})" using from_nat_into_surj assms by force |
536 moreover have "emeasure lborel (\<Union>i. {from_nat_into A i}) = 0" |
536 moreover have "emeasure lborel (\<Union>i. {from_nat_into A i}) = 0" |
537 by (rule emeasure_UN_eq_0) auto |
537 by (rule emeasure_UN_eq_0) auto |
538 ultimately have "emeasure lborel A \<le> 0" using emeasure_mono |
538 ultimately have "emeasure lborel A \<le> 0" using emeasure_mono |
539 by (metis assms bot.extremum_unique emeasure_empty image_eq_UN range_from_nat_into sets.empty_sets) |
539 by (smt UN_E emeasure_empty equalityI from_nat_into order_refl singletonD subsetI) |
540 thus ?thesis by (auto simp add: emeasure_le_0_iff) |
540 thus ?thesis by (auto simp add: emeasure_le_0_iff) |
541 qed |
541 qed |
542 |
542 |
543 lemma countable_imp_null_set_lborel: "countable A \<Longrightarrow> A \<in> null_sets lborel" |
543 lemma countable_imp_null_set_lborel: "countable A \<Longrightarrow> A \<in> null_sets lborel" |
544 by (simp add: null_sets_def emeasure_lborel_countable sets.countable) |
544 by (simp add: null_sets_def emeasure_lborel_countable sets.countable) |