src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy

     by (rule absolutely_integrable_spike) (auto intro: empty_imp_negligible)
   then show ?thesis
     unfolding absolutely_integrable_restrict_UNIV .
 qed
 
+lemma absolutely_integrable_on_combine:
+  fixes f :: "real \<Rightarrow> 'a::euclidean_space"
+  assumes "f absolutely_integrable_on {a..c}"
+    and "f absolutely_integrable_on {c..b}"
+    and "a \<le> c"
+    and "c \<le> b"
+  shows "f absolutely_integrable_on {a..b}"
+  by (metis absolutely_integrable_Un assms ivl_disj_un_two_touch(4))
+
 lemma uniform_limit_set_lebesgue_integral_at_top:
   fixes f :: "'a \<Rightarrow> real \<Rightarrow> 'b::{banach, second_countable_topology}"
     and g :: "real \<Rightarrow> real"
   assumes bound: "\<And>x y. x \<in> A \<Longrightarrow> y \<ge> a \<Longrightarrow> norm (f x y) \<le> g y"
   assumes integrable: "set_integrable M {a..} g"