--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Thu Sep 19 13:59:29 2019 +0100
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Thu Sep 19 14:49:19 2019 +0100
@@ -4844,6 +4844,15 @@
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"