# HG changeset patch
# User hoelzl
# Date 1475072151 -7200
# Node ID b235e845c8e8de31d9bd93544f9f7d9fbaf6f8a3
# Parent  51a3d38d2281af1d54adcc0eabeebeac2eb208f3
HOL-Analysis: add cover lemma ported by L. C. Paulson

diff -r 51a3d38d2281 -r b235e845c8e8 src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Thu Sep 29 12:58:55 2016 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Wed Sep 28 16:15:51 2016 +0200
@@ -16,6 +16,28 @@
 
 subsection \<open>Sundries\<close>
 
+
+text\<open>A transitive relation is well-founded if all initial segments are finite.\<close>
+lemma wf_finite_segments:
+  assumes "irrefl r" and "trans r" and "\<And>x. finite {y. (y, x) \<in> r}"
+  shows "wf (r)"
+  apply (simp add: trans_wf_iff wf_iff_acyclic_if_finite converse_def assms)
+  using acyclic_def assms irrefl_def trans_Restr by fastforce
+
+text\<open>For creating values between @{term u} and @{term v}.\<close>
+lemma scaling_mono:
+  fixes u::"'a::linordered_field"
+  assumes "u \<le> v" "0 \<le> r" "r \<le> s"
+    shows "u + r * (v - u) / s \<le> v"
+proof -
+  have "r/s \<le> 1" using assms
+    using divide_le_eq_1 by fastforce
+  then have "(r/s) * (v - u) \<le> 1 * (v - u)"
+    by (meson diff_ge_0_iff_ge mult_right_mono \<open>u \<le> v\<close>)
+  then show ?thesis
+    by (simp add: field_simps)
+qed
+
 lemma conjunctD2: assumes "a \<and> b" shows a b using assms by auto
 lemma conjunctD3: assumes "a \<and> b \<and> c" shows a b c using assms by auto
 lemma conjunctD4: assumes "a \<and> b \<and> c \<and> d" shows a b c d using assms by auto
@@ -4767,7 +4789,7 @@
 qed
 
 lemma negligible_Un_eq[simp]: "negligible (s \<union> t) \<longleftrightarrow> negligible s \<and> negligible t"
-  using negligible_Un negligible_subset by blast 
+  using negligible_Un negligible_subset by blast
 
 lemma negligible_sing[intro]: "negligible {a::'a::euclidean_space}"
   using negligible_standard_hyperplane[OF SOME_Basis, of "a \<bullet> (SOME i. i \<in> Basis)"] negligible_subset by blast
@@ -10709,6 +10731,277 @@
        (insert assms, simp_all add: powr_minus powr_realpow divide_simps)
 qed
 
+subsubsection \<open>Covering lemma\<close>
+
+
+text\<open> Some technical lemmas used in the approximation results that follow. Proof of the covering
+  lemma is an obvious multidimensional generalization of Lemma 3, p65 of Swartz's
+  "Introduction to Gauge Integrals". \<close>
+
+proposition covering_lemma:
+  assumes "S \<subseteq> cbox a b" "box a b \<noteq> {}" "gauge g"
+  obtains \<D> where
+    "countable \<D>"  "\<Union>\<D> \<subseteq> cbox a b"
+    "\<And>K. K \<in> \<D> \<Longrightarrow> interior K \<noteq> {} \<and> (\<exists>c d. K = cbox c d)"
+    "pairwise (\<lambda>A B. interior A \<inter> interior B = {}) \<D>"
+    "\<And>K. K \<in> \<D> \<Longrightarrow> \<exists>x \<in> S \<inter> K. K \<subseteq> g x"
+    "\<And>u v. cbox u v \<in> \<D> \<Longrightarrow> \<exists>n. \<forall>i \<in> Basis. v \<bullet> i - u \<bullet> i = (b \<bullet> i - a \<bullet> i) / 2^n"
+    "S \<subseteq> \<Union>\<D>"
+proof -
+  have aibi: "\<And>i. i \<in> Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i" and normab: "0 < norm(b - a)"
+    using \<open>box a b \<noteq> {}\<close> box_eq_empty box_sing by fastforce+
+  let ?K0 = "\<lambda>(n, f::'a\<Rightarrow>nat).
+                    cbox (\<Sum>i \<in> Basis. (a \<bullet> i + (f i / 2^n) * (b \<bullet> i - a \<bullet> i)) *\<^sub>R i)
+                         (\<Sum>i \<in> Basis. (a \<bullet> i + ((f i + 1) / 2^n) * (b \<bullet> i - a \<bullet> i)) *\<^sub>R i)"
+  let ?D0 = "?K0 ` (SIGMA n:UNIV. PiE Basis (\<lambda>i::'a. lessThan (2^n)))"
+  obtain \<D>0 where count: "countable \<D>0"
+             and sub: "\<Union>\<D>0 \<subseteq> cbox a b"
+             and int:  "\<And>K. K \<in> \<D>0 \<Longrightarrow> (interior K \<noteq> {}) \<and> (\<exists>c d. K = cbox c d)"
+             and intdj: "\<And>A B. \<lbrakk>A \<in> \<D>0; B \<in> \<D>0\<rbrakk> \<Longrightarrow> A \<subseteq> B \<or> B \<subseteq> A \<or> interior A \<inter> interior B = {}"
+             and SK: "\<And>x. x \<in> S \<Longrightarrow> \<exists>K \<in> \<D>0. x \<in> K \<and> K \<subseteq> g x"
+             and cbox: "\<And>u v. cbox u v \<in> \<D>0 \<Longrightarrow> \<exists>n. \<forall>i \<in> Basis. v \<bullet> i - u \<bullet> i = (b \<bullet> i - a \<bullet> i) / 2^n"
+             and fin: "\<And>K. K \<in> \<D>0 \<Longrightarrow> finite {L \<in> \<D>0. K \<subseteq> L}"
+  proof
+    show "countable ?D0"
+      by (simp add: countable_PiE)
+  next
+    show "\<Union>?D0 \<subseteq> cbox a b"
+      apply (simp add: UN_subset_iff)
+      apply (intro conjI allI ballI subset_box_imp)
+       apply (simp add: divide_simps zero_le_mult_iff aibi)
+      apply (force simp: aibi scaling_mono nat_less_real_le dest: PiE_mem)
+      done
+  next
+    show "\<And>K. K \<in> ?D0 \<Longrightarrow> interior K \<noteq> {} \<and> (\<exists>c d. K = cbox c d)"
+      using \<open>box a b \<noteq> {}\<close>
+      by (clarsimp simp: box_eq_empty) (fastforce simp add: divide_simps dest: PiE_mem)
+  next
+    have realff: "(real w) * 2^m < (real v) * 2^n \<longleftrightarrow> w * 2^m < v * 2^n" for m n v w
+      using of_nat_less_iff less_imp_of_nat_less by fastforce
+    have *: "\<forall>v w. ?K0(m,v) \<subseteq> ?K0(n,w) \<or> ?K0(n,w) \<subseteq> ?K0(m,v) \<or> interior(?K0(m,v)) \<inter> interior(?K0(n,w)) = {}"
+      for m n --\<open>The symmetry argument requires a single HOL formula\<close>
+    proof (rule linorder_wlog [where a=m and b=n], intro allI impI)
+      fix v w m and n::nat
+      assume "m \<le> n" --\<open>WLOG we can assume @{term"m \<le> n"}, when the first disjunct becomes impossible\<close>
+      have "?K0(n,w) \<subseteq> ?K0(m,v) \<or> interior(?K0(m,v)) \<inter> interior(?K0(n,w)) = {}"
+        apply (simp add: subset_box disjoint_interval)
+        apply (rule ccontr)
+        apply (clarsimp simp add: aibi mult_le_cancel_right divide_le_cancel not_less not_le)
+        apply (drule_tac x=i in bspec, assumption)
+        using \<open>m\<le>n\<close> realff [of _ _ "1+_"] realff [of "1+_"_ "1+_"]
+        apply (auto simp: divide_simps add.commute not_le nat_le_iff_add realff)
+        apply (simp add: power_add, metis (no_types, hide_lams) mult_Suc mult_less_cancel2 not_less_eq mult.assoc)+
+        done
+      then show "?K0(m,v) \<subseteq> ?K0(n,w) \<or> ?K0(n,w) \<subseteq> ?K0(m,v) \<or> interior(?K0(m,v)) \<inter> interior(?K0(n,w)) = {}"
+        by meson
+    qed auto
+    show "\<And>A B. \<lbrakk>A \<in> ?D0; B \<in> ?D0\<rbrakk> \<Longrightarrow> A \<subseteq> B \<or> B \<subseteq> A \<or> interior A \<inter> interior B = {}"
+      apply (erule imageE SigmaE)+
+      using * by simp
+  next
+    show "\<exists>K \<in> ?D0. x \<in> K \<and> K \<subseteq> g x" if "x \<in> S" for x
+    proof (simp only: bex_simps split_paired_Bex_Sigma)
+      show "\<exists>n. \<exists>f \<in> Basis \<rightarrow>\<^sub>E {..<2 ^ n}. x \<in> ?K0(n,f) \<and> ?K0(n,f) \<subseteq> g x"
+      proof -
+        obtain e where "0 < e"
+                   and e: "\<And>y. (\<And>i. i \<in> Basis \<Longrightarrow> \<bar>x \<bullet> i - y \<bullet> i\<bar> \<le> e) \<Longrightarrow> y \<in> g x"
+        proof -
+          have "x \<in> g x" "open (g x)"
+            using \<open>gauge g\<close> by (auto simp: gauge_def)
+          then obtain \<epsilon> where "0 < \<epsilon>" and \<epsilon>: "ball x \<epsilon> \<subseteq> g x"
+            using openE by blast
+          have "norm (x - y) < \<epsilon>"
+               if "(\<And>i. i \<in> Basis \<Longrightarrow> \<bar>x \<bullet> i - y \<bullet> i\<bar> \<le> \<epsilon> / (2 * real DIM('a)))" for y
+          proof -
+            have "norm (x - y) \<le> (\<Sum>i\<in>Basis. \<bar>x \<bullet> i - y \<bullet> i\<bar>)"
+              by (metis (no_types, lifting) inner_diff_left norm_le_l1 setsum.cong)
+            also have "... \<le> DIM('a) * (\<epsilon> / (2 * real DIM('a)))"
+              by (meson setsum_bounded_above that)
+            also have "... = \<epsilon> / 2"
+              by (simp add: divide_simps)
+            also have "... < \<epsilon>"
+              by (simp add: \<open>0 < \<epsilon>\<close>)
+            finally show ?thesis .
+          qed
+          then show ?thesis
+            by (rule_tac e = "\<epsilon> / 2 / DIM('a)" in that) (simp_all add:  \<open>0 < \<epsilon>\<close> dist_norm subsetD [OF \<epsilon>])
+        qed
+        have xab: "x \<in> cbox a b"
+          using \<open>x \<in> S\<close> \<open>S \<subseteq> cbox a b\<close> by blast
+        obtain n where n: "norm (b - a) / 2^n < e"
+          using real_arch_pow_inv [of "e / norm(b - a)" "1/2"] normab \<open>0 < e\<close>
+          by (auto simp: divide_simps)
+        then have "norm (b - a) < e * 2^n"
+          by (auto simp: divide_simps)
+        then have bai: "b \<bullet> i - a \<bullet> i < e * 2 ^ n" if "i \<in> Basis" for i
+        proof -
+          have "b \<bullet> i - a \<bullet> i \<le> norm (b - a)"
+            by (metis abs_of_nonneg dual_order.trans inner_diff_left linear norm_ge_zero Basis_le_norm that)
+          also have "... < e * 2 ^ n"
+            using \<open>norm (b - a) < e * 2 ^ n\<close> by blast
+          finally show ?thesis .
+        qed
+        have D: "(a + n \<le> x \<and> x \<le> a + m) \<Longrightarrow> (a + n \<le> y \<and> y \<le> a + m) \<Longrightarrow> abs(x - y) \<le> m - n"
+                 for a m n x and y::real
+          by auto
+        have "\<forall>i\<in>Basis. \<exists>k<2 ^ n. (a \<bullet> i + real k * (b \<bullet> i - a \<bullet> i) / 2 ^ n \<le> x \<bullet> i \<and>
+               x \<bullet> i \<le> a \<bullet> i + (real k + 1) * (b \<bullet> i - a \<bullet> i) / 2 ^ n)"
+        proof
+          fix i::'a assume "i \<in> Basis"
+          consider "x \<bullet> i = b \<bullet> i" | "x \<bullet> i < b \<bullet> i"
+            using \<open>i \<in> Basis\<close> mem_box(2) xab by force
+          then show "\<exists>k<2 ^ n. (a \<bullet> i + real k * (b \<bullet> i - a \<bullet> i) / 2 ^ n \<le> x \<bullet> i \<and>
+                          x \<bullet> i \<le> a \<bullet> i + (real k + 1) * (b \<bullet> i - a \<bullet> i) / 2 ^ n)"
+          proof cases
+            case 1 then show ?thesis
+              by (rule_tac x = "2^n - 1" in exI) (auto simp: algebra_simps divide_simps of_nat_diff \<open>i \<in> Basis\<close> aibi)
+          next
+            case 2
+            then have abi_less: "a \<bullet> i < b \<bullet> i"
+              using \<open>i \<in> Basis\<close> xab by (auto simp: mem_box)
+            let ?k = "nat \<lfloor>2 ^ n * (x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i)\<rfloor>"
+            show ?thesis
+            proof (intro exI conjI)
+              show "?k < 2 ^ n"
+                using aibi xab \<open>i \<in> Basis\<close>
+                by (force simp: nat_less_iff floor_less_iff divide_simps 2 mem_box)
+            next
+              have "a \<bullet> i + real ?k * (b \<bullet> i - a \<bullet> i) / 2 ^ n \<le>
+                    a \<bullet> i + (2 ^ n * (x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i)) * (b \<bullet> i - a \<bullet> i) / 2 ^ n"
+                apply (intro add_left_mono mult_right_mono divide_right_mono of_nat_floor)
+                using aibi [OF \<open>i \<in> Basis\<close>] xab 2
+                  apply (simp_all add: \<open>i \<in> Basis\<close> mem_box divide_simps)
+                done
+              also have "... = x \<bullet> i"
+                using abi_less by (simp add: divide_simps)
+              finally show "a \<bullet> i + real ?k * (b \<bullet> i - a \<bullet> i) / 2 ^ n \<le> x \<bullet> i" .
+            next
+              have "x \<bullet> i \<le> a \<bullet> i + (2 ^ n * (x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i)) * (b \<bullet> i - a \<bullet> i) / 2 ^ n"
+                using abi_less by (simp add: divide_simps algebra_simps)
+              also have "... \<le> a \<bullet> i + (real ?k + 1) * (b \<bullet> i - a \<bullet> i) / 2 ^ n"
+                apply (intro add_left_mono mult_right_mono divide_right_mono of_nat_floor)
+                using aibi [OF \<open>i \<in> Basis\<close>] xab
+                  apply (auto simp: \<open>i \<in> Basis\<close> mem_box divide_simps)
+                done
+              finally show "x \<bullet> i \<le> a \<bullet> i + (real ?k + 1) * (b \<bullet> i - a \<bullet> i) / 2 ^ n" .
+            qed
+          qed
+        qed
+        then have "\<exists>f\<in>Basis \<rightarrow>\<^sub>E {..<2 ^ n}. x \<in> ?K0(n,f)"
+          apply (simp add: mem_box Bex_def)
+          apply (clarify dest!: bchoice)
+          apply (rule_tac x="restrict f Basis" in exI, simp)
+          done
+        moreover have "\<And>f. x \<in> ?K0(n,f) \<Longrightarrow> ?K0(n,f) \<subseteq> g x"
+          apply (clarsimp simp add: mem_box)
+          apply (rule e)
+          apply (drule bspec D, assumption)+
+          apply (erule order_trans)
+          apply (simp add: divide_simps)
+          using bai by (force simp: algebra_simps)
+        ultimately show ?thesis by auto
+      qed
+    qed
+  next
+    show "\<And>u v. cbox u v \<in> ?D0 \<Longrightarrow> \<exists>n. \<forall>i \<in> Basis. v \<bullet> i - u \<bullet> i = (b \<bullet> i - a \<bullet> i) / 2^n"
+      by (force simp: eq_cbox box_eq_empty field_simps dest!: aibi)
+  next
+    obtain j::'a where "j \<in> Basis"
+      using nonempty_Basis by blast
+    have "finite {L \<in> ?D0. ?K0(n,f) \<subseteq> L}" if "f \<in> Basis \<rightarrow>\<^sub>E {..<2 ^ n}" for n f
+    proof (rule finite_subset)
+      let ?B = "(\<lambda>(n, f::'a\<Rightarrow>nat). cbox (\<Sum>i\<in>Basis. (a \<bullet> i + (f i) / 2^n * (b \<bullet> i - a \<bullet> i)) *\<^sub>R i)
+                                        (\<Sum>i\<in>Basis. (a \<bullet> i + ((f i) + 1) / 2^n * (b \<bullet> i - a \<bullet> i)) *\<^sub>R i))
+                ` (SIGMA m:atMost n. PiE Basis (\<lambda>i::'a. lessThan (2^m)))"
+      have "?K0(m,g) \<in> ?B" if "g \<in> Basis \<rightarrow>\<^sub>E {..<2 ^ m}" "?K0(n,f) \<subseteq> ?K0(m,g)" for m g
+      proof -
+        have dd: "w / m \<le> v / n \<and> (v+1) / n \<le> (w+1) / m
+                  \<Longrightarrow> inverse n \<le> inverse m" for w m v n::real
+          by (auto simp: divide_simps algebra_simps)
+        have bjaj: "b \<bullet> j - a \<bullet> j > 0"
+          using \<open>j \<in> Basis\<close> \<open>box a b \<noteq> {}\<close> box_eq_empty(1) by fastforce
+        have "((g j) / 2 ^ m) * (b \<bullet> j - a \<bullet> j) \<le> ((f j) / 2 ^ n) * (b \<bullet> j - a \<bullet> j) \<and>
+              (((f j) + 1) / 2 ^ n) * (b \<bullet> j - a \<bullet> j) \<le> (((g j) + 1) / 2 ^ m) * (b \<bullet> j - a \<bullet> j)"
+          using that \<open>j \<in> Basis\<close> by (simp add: subset_box algebra_simps divide_simps aibi)
+        then have "((g j) / 2 ^ m) \<le> ((f j) / 2 ^ n) \<and>
+          ((real(f j) + 1) / 2 ^ n) \<le> ((real(g j) + 1) / 2 ^ m)"
+          by (metis bjaj mult.commute of_nat_1 of_nat_add real_mult_le_cancel_iff2)
+        then have "inverse (2^n) \<le> (inverse (2^m) :: real)"
+          by (rule dd)
+        then have "m \<le> n"
+          by auto
+        show ?thesis
+          by (rule imageI) (simp add: \<open>m \<le> n\<close> that)
+      qed
+      then show "{L \<in> ?D0. ?K0(n,f) \<subseteq> L} \<subseteq> ?B"
+        by auto
+      show "finite ?B"
+        by (intro finite_imageI finite_SigmaI finite_atMost finite_lessThan finite_PiE finite_Basis)
+    qed
+    then show "finite {L \<in> ?D0. K \<subseteq> L}" if "K \<in> ?D0" for K
+      using that by auto
+  qed
+  let ?D1 = "{K \<in> \<D>0. \<exists>x \<in> S \<inter> K. K \<subseteq> g x}"
+  obtain \<D> where count: "countable \<D>"
+             and sub: "\<Union>\<D> \<subseteq> cbox a b"  "S \<subseteq> \<Union>\<D>"
+             and int:  "\<And>K. K \<in> \<D> \<Longrightarrow> (interior K \<noteq> {}) \<and> (\<exists>c d. K = cbox c d)"
+             and intdj: "\<And>A B. \<lbrakk>A \<in> \<D>; B \<in> \<D>\<rbrakk> \<Longrightarrow> A \<subseteq> B \<or> B \<subseteq> A \<or> interior A \<inter> interior B = {}"
+             and SK: "\<And>K. K \<in> \<D> \<Longrightarrow> \<exists>x. x \<in> S \<inter> K \<and> K \<subseteq> g x"
+             and cbox: "\<And>u v. cbox u v \<in> \<D> \<Longrightarrow> \<exists>n. \<forall>i \<in> Basis. v \<bullet> i - u \<bullet> i = (b \<bullet> i - a \<bullet> i) / 2^n"
+             and fin: "\<And>K. K \<in> \<D> \<Longrightarrow> finite {L. L \<in> \<D> \<and> K \<subseteq> L}"
+  proof
+    show "countable ?D1" using count countable_subset
+      by (simp add: count countable_subset)
+    show "\<Union>?D1 \<subseteq> cbox a b"
+      using sub by blast
+    show "S \<subseteq> \<Union>?D1"
+      using SK by (force simp:)
+    show "\<And>K. K \<in> ?D1 \<Longrightarrow> (interior K \<noteq> {}) \<and> (\<exists>c d. K = cbox c d)"
+      using int by blast
+    show "\<And>A B. \<lbrakk>A \<in> ?D1; B \<in> ?D1\<rbrakk> \<Longrightarrow> A \<subseteq> B \<or> B \<subseteq> A \<or> interior A \<inter> interior B = {}"
+      using intdj by blast
+    show "\<And>K. K \<in> ?D1 \<Longrightarrow> \<exists>x. x \<in> S \<inter> K \<and> K \<subseteq> g x"
+      by auto
+    show "\<And>u v. cbox u v \<in> ?D1 \<Longrightarrow> \<exists>n. \<forall>i \<in> Basis. v \<bullet> i - u \<bullet> i = (b \<bullet> i - a \<bullet> i) / 2^n"
+      using cbox by blast
+    show "\<And>K. K \<in> ?D1 \<Longrightarrow> finite {L. L \<in> ?D1 \<and> K \<subseteq> L}"
+      using fin by simp (metis (mono_tags, lifting) Collect_mono rev_finite_subset)
+  qed
+  let ?\<D> = "{K \<in> \<D>. \<forall>K'. K' \<in> \<D> \<and> K \<noteq> K' \<longrightarrow> ~(K \<subseteq> K')}"
+  show ?thesis
+  proof (rule that)
+    show "countable ?\<D>"
+      by (blast intro: countable_subset [OF _ count])
+    show "\<Union>?\<D> \<subseteq> cbox a b"
+      using sub by blast
+    show "S \<subseteq> \<Union>?\<D>"
+    proof clarsimp
+      fix x
+      assume "x \<in> S"
+      then obtain X where "x \<in> X" "X \<in> \<D>" using \<open>S \<subseteq> \<Union>\<D>\<close> by blast
+      let ?R = "{(K,L). K \<in> \<D> \<and> L \<in> \<D> \<and> L \<subset> K}"
+      have irrR: "irrefl ?R" by (force simp: irrefl_def)
+      have traR: "trans ?R" by (force simp: trans_def)
+      have finR: "\<And>x. finite {y. (y, x) \<in> ?R}"
+        by simp (metis (mono_tags, lifting) fin \<open>X \<in> \<D>\<close> finite_subset mem_Collect_eq psubset_imp_subset subsetI)
+      have "{X \<in> \<D>. x \<in> X} \<noteq> {}"
+        using \<open>X \<in> \<D>\<close> \<open>x \<in> X\<close> by blast
+      then obtain Y where "Y \<in> {X \<in> \<D>. x \<in> X}" "\<And>Y'. (Y', Y) \<in> ?R \<Longrightarrow> Y' \<notin> {X \<in> \<D>. x \<in> X}"
+        by (rule wfE_min' [OF wf_finite_segments [OF irrR traR finR]]) blast
+      then show "\<exists>Y. Y \<in> \<D> \<and> (\<forall>K'. K' \<in> \<D> \<and> Y \<noteq> K' \<longrightarrow> \<not> Y \<subseteq> K') \<and> x \<in> Y"
+        by blast
+    qed
+    show "\<And>K. K \<in> ?\<D> \<Longrightarrow> interior K \<noteq> {} \<and> (\<exists>c d. K = cbox c d)"
+      by (blast intro: dest: int)
+    show "pairwise (\<lambda>A B. interior A \<inter> interior B = {}) ?\<D>"
+      using intdj by (simp add: pairwise_def) metis
+    show "\<And>K. K \<in> ?\<D> \<Longrightarrow> \<exists>x \<in> S \<inter> K. K \<subseteq> g x"
+      using SK by force
+    show "\<And>u v. cbox u v \<in> ?\<D> \<Longrightarrow> \<exists>n. \<forall>i\<in>Basis. v \<bullet> i - u \<bullet> i = (b \<bullet> i - a \<bullet> i) / 2^n"
+      using cbox by force
+    qed
+qed
+
 subsubsection \<open>Adaption to ordered Euclidean spaces and the Cartesian Euclidean space\<close>
 
 lemma integral_component_eq_cart[simp]: