--- a/src/HOL/Analysis/Lebesgue_Measure.thy Sun Apr 15 13:57:00 2018 +0100
+++ b/src/HOL/Analysis/Lebesgue_Measure.thy Sun Apr 15 17:22:47 2018 +0100
@@ -936,7 +936,6 @@
from continuous_attains_sup[OF \<open>compact S\<close> \<open>S \<noteq> {}\<close> this]
obtain M where M: "\<And>x. x \<in> S \<Longrightarrow> norm (f x) \<le> M"
by auto
-
show ?thesis
proof (rule integrable_bound)
show "integrable lborel (\<lambda>x. indicator S x * M)"
@@ -962,6 +961,8 @@
by (auto simp: mult.commute)
qed
+subsection\<open>Lebesgue measurable sets\<close>
+
abbreviation lmeasurable :: "'a::euclidean_space set set"
where
"lmeasurable \<equiv> fmeasurable lebesgue"
@@ -999,6 +1000,10 @@
by (auto dest!: AE_not_in)
qed
+lemma bounded_set_imp_lmeasurable:
+ assumes "bounded S" "S \<in> sets lebesgue" shows "S \<in> lmeasurable"
+ by (metis assms bounded_Un emeasure_bounded_finite emeasure_completion fmeasurableI main_part_null_part_Un)
+
subsection \<open>A nice lemma for negligibility proofs\<close>
lemma summable_iff_suminf_neq_top: "(\<And>n. f n \<ge> 0) \<Longrightarrow> \<not> summable f \<Longrightarrow> (\<Sum>i. ennreal (f i)) = top"