--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Tue Aug 27 23:12:28 2019 +0200
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Wed Aug 28 00:08:14 2019 +0200
@@ -5,7 +5,7 @@
*)
theory Equivalence_Lebesgue_Henstock_Integration
- imports Lebesgue_Measure Henstock_Kurzweil_Integration Complete_Measure Set_Integral
+ imports Lebesgue_Measure Henstock_Kurzweil_Integration Complete_Measure Set_Integral Homeomorphism
begin
lemma le_left_mono: "x \<le> y \<Longrightarrow> y \<le> a \<longrightarrow> x \<le> (a::'a::preorder)"