diff -r 8a7053892d8e -r 2b0dca68c3ee src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Thu Jul 18 14:08:44 2019 +0100
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Thu Jul 18 15:40:15 2019 +0100
@@ -957,6 +957,11 @@
     using absolutely_integrable_on_def set_integrable_def by blast
 qed
 
+lemma absolutely_integrable_imp_integrable:
+  assumes "f absolutely_integrable_on S" "S \<in> sets lebesgue"
+  shows "integrable (lebesgue_on S) f"
+  by (meson assms integrable_restrict_space set_integrable_def sets.Int sets.top)
+
 lemma absolutely_integrable_on_null [intro]:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   shows "content (cbox a b) = 0 \<Longrightarrow> f absolutely_integrable_on (cbox a b)"