# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1568900959 -3600
# Node ID 91587befabfd945eb3554d26179e9718564cbf8e
# Parent  e19c18b4a0ddc3fae852881c8342bad02f4374f9
one small last theorem

diff -r e19c18b4a0dd -r 91587befabfd src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
--- 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"