src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy

   have "integrable lebesgue (\<lambda>x. indicator S x *\<^sub>R f x)"
     using S f inf_top.comm_neutral integrable_restrict_space by blast
   then show ?thesis
     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)"
   by (auto simp: absolutely_integrable_on_def)