--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy Wed Sep 28 16:15:51 2016 +0200
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy Thu Sep 29 13:02:43 2016 +0200
@@ -6417,6 +6417,26 @@
unfolding segment_convex_hull
by (auto intro!: hull_subset[unfolded subset_eq, rule_format])
+lemma eventually_closed_segment:
+ fixes x0::"'a::real_normed_vector"
+ assumes "open X0" "x0 \<in> X0"
+ shows "\<forall>\<^sub>F x in at x0 within U. closed_segment x0 x \<subseteq> X0"
+proof -
+ from openE[OF assms]
+ obtain e where e: "0 < e" "ball x0 e \<subseteq> X0" .
+ then have "\<forall>\<^sub>F x in at x0 within U. x \<in> ball x0 e"
+ by (auto simp: dist_commute eventually_at)
+ then show ?thesis
+ proof eventually_elim
+ case (elim x)
+ have "x0 \<in> ball x0 e" using \<open>e > 0\<close> by simp
+ from convex_ball[unfolded convex_contains_segment, rule_format, OF this elim]
+ have "closed_segment x0 x \<subseteq> ball x0 e" .
+ also note \<open>\<dots> \<subseteq> X0\<close>
+ finally show ?case .
+ qed
+qed
+
lemma segment_furthest_le:
fixes a b x y :: "'a::euclidean_space"
assumes "x \<in> closed_segment a b"
@@ -10500,7 +10520,7 @@
lemma collinear_3_expand:
"collinear{a,b,c} \<longleftrightarrow> a = c \<or> (\<exists>u. b = u *\<^sub>R a + (1 - u) *\<^sub>R c)"
-proof -
+proof -
have "collinear{a,b,c} = collinear{a,c,b}"
by (simp add: insert_commute)
also have "... = collinear {0, a - c, b - c}"
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Wed Sep 28 16:15:51 2016 +0200
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Thu Sep 29 13:02:43 2016 +0200
@@ -6,201 +6,49 @@
theory Henstock_Kurzweil_Integration
imports
- Lebesgue_Measure
+ Lebesgue_Measure Tagged_Division
begin
-lemmas scaleR_simps = scaleR_zero_left scaleR_minus_left scaleR_left_diff_distrib
- scaleR_zero_right scaleR_minus_right scaleR_right_diff_distrib scaleR_eq_0_iff
- scaleR_cancel_left scaleR_cancel_right scaleR_add_right scaleR_add_left real_vector_class.scaleR_one
-
-
-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"
+(* BEGIN MOVE *)
+lemma swap_continuous:
+ assumes "continuous_on (cbox (a,c) (b,d)) (\<lambda>(x,y). f x y)"
+ shows "continuous_on (cbox (c,a) (d,b)) (\<lambda>(x, y). f y x)"
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>)
+ have "(\<lambda>(x, y). f y x) = (\<lambda>(x, y). f x y) \<circ> prod.swap"
+ by auto
then show ?thesis
- by (simp add: field_simps)
+ apply (rule ssubst)
+ apply (rule continuous_on_compose)
+ apply (simp add: split_def)
+ apply (rule continuous_intros | simp add: assms)+
+ done
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
-
-lemma cond_cases: "(P \<Longrightarrow> Q x) \<Longrightarrow> (\<not> P \<Longrightarrow> Q y) \<Longrightarrow> Q (if P then x else y)"
+
+lemma norm_minus2: "norm (x1-x2, y1-y2) = norm (x2-x1, y2-y1)"
+ by (simp add: norm_minus_eqI)
+
+lemma norm_diff2: "\<lbrakk>y = y1 + y2; x = x1 + x2; e = e1 + e2; norm(y1 - x1) \<le> e1; norm(y2 - x2) \<le> e2\<rbrakk>
+ \<Longrightarrow> norm(y - x) \<le> e"
+ using norm_triangle_mono [of "y1 - x1" "e1" "y2 - x2" "e2"]
+ by (simp add: add_diff_add)
+
+lemma setcomp_dot1: "{z. P (z \<bullet> (i,0))} = {(x,y). P(x \<bullet> i)}"
by auto
-declare norm_triangle_ineq4[intro]
-
-lemma transitive_stepwise_le:
- assumes "\<And>x. R x x" "\<And>x y z. R x y \<Longrightarrow> R y z \<Longrightarrow> R x z" and "\<And>n. R n (Suc n)"
- shows "\<forall>n\<ge>m. R m n"
-proof (intro allI impI)
- show "m \<le> n \<Longrightarrow> R m n" for n
- by (induction rule: dec_induct)
- (use assms in blast)+
-qed
-
-subsection \<open>Some useful lemmas about intervals.\<close>
+lemma setcomp_dot2: "{z. P (z \<bullet> (0,i))} = {(x,y). P(y \<bullet> i)}"
+ by auto
+
+lemma Sigma_Int_Paircomp1: "(Sigma A B) \<inter> {(x, y). P x} = Sigma (A \<inter> {x. P x}) B"
+ by blast
+
+lemma Sigma_Int_Paircomp2: "(Sigma A B) \<inter> {(x, y). P y} = Sigma A (\<lambda>z. B z \<inter> {y. P y})"
+ by blast
lemma empty_as_interval: "{} = cbox One (0::'a::euclidean_space)"
using nonempty_Basis
by (fastforce simp add: set_eq_iff mem_box)
-
-lemma interior_subset_union_intervals:
- assumes "i = cbox a b"
- and "j = cbox c d"
- and "interior j \<noteq> {}"
- and "i \<subseteq> j \<union> s"
- and "interior i \<inter> interior j = {}"
- shows "interior i \<subseteq> interior s"
-proof -
- have "box a b \<inter> cbox c d = {}"
- using inter_interval_mixed_eq_empty[of c d a b] and assms(3,5)
- unfolding assms(1,2) interior_cbox by auto
- moreover
- have "box a b \<subseteq> cbox c d \<union> s"
- apply (rule order_trans,rule box_subset_cbox)
- using assms(4) unfolding assms(1,2)
- apply auto
- done
- ultimately
- show ?thesis
- unfolding assms interior_cbox
- by auto (metis IntI UnE empty_iff interior_maximal open_box subsetCE subsetI)
-qed
-
-lemma interior_Union_subset_cbox:
- assumes "finite f"
- assumes f: "\<And>s. s \<in> f \<Longrightarrow> \<exists>a b. s = cbox a b" "\<And>s. s \<in> f \<Longrightarrow> interior s \<subseteq> t"
- and t: "closed t"
- shows "interior (\<Union>f) \<subseteq> t"
-proof -
- have [simp]: "s \<in> f \<Longrightarrow> closed s" for s
- using f by auto
- define E where "E = {s\<in>f. interior s = {}}"
- then have "finite E" "E \<subseteq> {s\<in>f. interior s = {}}"
- using \<open>finite f\<close> by auto
- then have "interior (\<Union>f) = interior (\<Union>(f - E))"
- proof (induction E rule: finite_subset_induct')
- case (insert s f')
- have "interior (\<Union>(f - insert s f') \<union> s) = interior (\<Union>(f - insert s f'))"
- using insert.hyps \<open>finite f\<close> by (intro interior_closed_Un_empty_interior) auto
- also have "\<Union>(f - insert s f') \<union> s = \<Union>(f - f')"
- using insert.hyps by auto
- finally show ?case
- by (simp add: insert.IH)
- qed simp
- also have "\<dots> \<subseteq> \<Union>(f - E)"
- by (rule interior_subset)
- also have "\<dots> \<subseteq> t"
- proof (rule Union_least)
- fix s assume "s \<in> f - E"
- with f[of s] obtain a b where s: "s \<in> f" "s = cbox a b" "box a b \<noteq> {}"
- by (fastforce simp: E_def)
- have "closure (interior s) \<subseteq> closure t"
- by (intro closure_mono f \<open>s \<in> f\<close>)
- with s \<open>closed t\<close> show "s \<subseteq> t"
- by (simp add: closure_box)
- qed
- finally show ?thesis .
-qed
-
-lemma inter_interior_unions_intervals:
- "finite f \<Longrightarrow> open s \<Longrightarrow> \<forall>t\<in>f. \<exists>a b. t = cbox a b \<Longrightarrow> \<forall>t\<in>f. s \<inter> (interior t) = {} \<Longrightarrow> s \<inter> interior (\<Union>f) = {}"
- using interior_Union_subset_cbox[of f "UNIV - s"] by auto
-
-lemma interval_split:
- fixes a :: "'a::euclidean_space"
- assumes "k \<in> Basis"
- shows
- "cbox a b \<inter> {x. x\<bullet>k \<le> c} = cbox a (\<Sum>i\<in>Basis. (if i = k then min (b\<bullet>k) c else b\<bullet>i) *\<^sub>R i)"
- "cbox a b \<inter> {x. x\<bullet>k \<ge> c} = cbox (\<Sum>i\<in>Basis. (if i = k then max (a\<bullet>k) c else a\<bullet>i) *\<^sub>R i) b"
- apply (rule_tac[!] set_eqI)
- unfolding Int_iff mem_box mem_Collect_eq
- using assms
- apply auto
- done
-
-lemma interval_not_empty: "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i \<Longrightarrow> cbox a b \<noteq> {}"
- by (simp add: box_ne_empty)
-
-subsection \<open>Bounds on intervals where they exist.\<close>
-
-definition interval_upperbound :: "('a::euclidean_space) set \<Rightarrow> 'a"
- where "interval_upperbound s = (\<Sum>i\<in>Basis. (SUP x:s. x\<bullet>i) *\<^sub>R i)"
-
-definition interval_lowerbound :: "('a::euclidean_space) set \<Rightarrow> 'a"
- where "interval_lowerbound s = (\<Sum>i\<in>Basis. (INF x:s. x\<bullet>i) *\<^sub>R i)"
-
-lemma interval_upperbound[simp]:
- "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i \<Longrightarrow>
- interval_upperbound (cbox a b) = (b::'a::euclidean_space)"
- unfolding interval_upperbound_def euclidean_representation_setsum cbox_def
- by (safe intro!: cSup_eq) auto
-
-lemma interval_lowerbound[simp]:
- "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i \<Longrightarrow>
- interval_lowerbound (cbox a b) = (a::'a::euclidean_space)"
- unfolding interval_lowerbound_def euclidean_representation_setsum cbox_def
- by (safe intro!: cInf_eq) auto
-
-lemmas interval_bounds = interval_upperbound interval_lowerbound
-
-lemma
- fixes X::"real set"
- shows interval_upperbound_real[simp]: "interval_upperbound X = Sup X"
- and interval_lowerbound_real[simp]: "interval_lowerbound X = Inf X"
- by (auto simp: interval_upperbound_def interval_lowerbound_def)
-
-lemma interval_bounds'[simp]:
- assumes "cbox a b \<noteq> {}"
- shows "interval_upperbound (cbox a b) = b"
- and "interval_lowerbound (cbox a b) = a"
- using assms unfolding box_ne_empty by auto
-
-lemma interval_upperbound_Times:
- assumes "A \<noteq> {}" and "B \<noteq> {}"
- shows "interval_upperbound (A \<times> B) = (interval_upperbound A, interval_upperbound B)"
-proof-
- from assms have fst_image_times': "A = fst ` (A \<times> B)" by simp
- have "(\<Sum>i\<in>Basis. (SUP x:A \<times> B. x \<bullet> (i, 0)) *\<^sub>R i) = (\<Sum>i\<in>Basis. (SUP x:A. x \<bullet> i) *\<^sub>R i)"
- by (subst (2) fst_image_times') (simp del: fst_image_times add: o_def inner_Pair_0)
- moreover from assms have snd_image_times': "B = snd ` (A \<times> B)" by simp
- have "(\<Sum>i\<in>Basis. (SUP x:A \<times> B. x \<bullet> (0, i)) *\<^sub>R i) = (\<Sum>i\<in>Basis. (SUP x:B. x \<bullet> i) *\<^sub>R i)"
- by (subst (2) snd_image_times') (simp del: snd_image_times add: o_def inner_Pair_0)
- ultimately show ?thesis unfolding interval_upperbound_def
- by (subst setsum_Basis_prod_eq) (auto simp add: setsum_prod)
-qed
-
-lemma interval_lowerbound_Times:
- assumes "A \<noteq> {}" and "B \<noteq> {}"
- shows "interval_lowerbound (A \<times> B) = (interval_lowerbound A, interval_lowerbound B)"
-proof-
- from assms have fst_image_times': "A = fst ` (A \<times> B)" by simp
- have "(\<Sum>i\<in>Basis. (INF x:A \<times> B. x \<bullet> (i, 0)) *\<^sub>R i) = (\<Sum>i\<in>Basis. (INF x:A. x \<bullet> i) *\<^sub>R i)"
- by (subst (2) fst_image_times') (simp del: fst_image_times add: o_def inner_Pair_0)
- moreover from assms have snd_image_times': "B = snd ` (A \<times> B)" by simp
- have "(\<Sum>i\<in>Basis. (INF x:A \<times> B. x \<bullet> (0, i)) *\<^sub>R i) = (\<Sum>i\<in>Basis. (INF x:B. x \<bullet> i) *\<^sub>R i)"
- by (subst (2) snd_image_times') (simp del: snd_image_times add: o_def inner_Pair_0)
- ultimately show ?thesis unfolding interval_lowerbound_def
- by (subst setsum_Basis_prod_eq) (auto simp add: setsum_prod)
-qed
+(* END MOVE *)
subsection \<open>Content (length, area, volume...) of an interval.\<close>
@@ -322,1508 +170,34 @@
by (auto simp: not_le)
qed
-subsection \<open>The notion of a gauge --- simply an open set containing the point.\<close>
-
-definition "gauge d \<longleftrightarrow> (\<forall>x. x \<in> d x \<and> open (d x))"
-
-lemma gaugeI:
- assumes "\<And>x. x \<in> g x"
- and "\<And>x. open (g x)"
- shows "gauge g"
- using assms unfolding gauge_def by auto
-
-lemma gaugeD[dest]:
- assumes "gauge d"
- shows "x \<in> d x"
- and "open (d x)"
- using assms unfolding gauge_def by auto
-
-lemma gauge_ball_dependent: "\<forall>x. 0 < e x \<Longrightarrow> gauge (\<lambda>x. ball x (e x))"
- unfolding gauge_def by auto
-
-lemma gauge_ball[intro]: "0 < e \<Longrightarrow> gauge (\<lambda>x. ball x e)"
- unfolding gauge_def by auto
-
-lemma gauge_trivial[intro!]: "gauge (\<lambda>x. ball x 1)"
- by (rule gauge_ball) auto
-
-lemma gauge_inter[intro]: "gauge d1 \<Longrightarrow> gauge d2 \<Longrightarrow> gauge (\<lambda>x. d1 x \<inter> d2 x)"
- unfolding gauge_def by auto
-
-lemma gauge_inters:
- assumes "finite s"
- and "\<forall>d\<in>s. gauge (f d)"
- shows "gauge (\<lambda>x. \<Inter>{f d x | d. d \<in> s})"
-proof -
- have *: "\<And>x. {f d x |d. d \<in> s} = (\<lambda>d. f d x) ` s"
- by auto
- show ?thesis
- unfolding gauge_def unfolding *
- using assms unfolding Ball_def Inter_iff mem_Collect_eq gauge_def by auto
-qed
-
-lemma gauge_existence_lemma:
- "(\<forall>x. \<exists>d :: real. p x \<longrightarrow> 0 < d \<and> q d x) \<longleftrightarrow> (\<forall>x. \<exists>d>0. p x \<longrightarrow> q d x)"
- by (metis zero_less_one)
-
-
-subsection \<open>Divisions.\<close>
-
-definition division_of (infixl "division'_of" 40)
-where
- "s division_of i \<longleftrightarrow>
- finite s \<and>
- (\<forall>k\<in>s. k \<subseteq> i \<and> k \<noteq> {} \<and> (\<exists>a b. k = cbox a b)) \<and>
- (\<forall>k1\<in>s. \<forall>k2\<in>s. k1 \<noteq> k2 \<longrightarrow> interior(k1) \<inter> interior(k2) = {}) \<and>
- (\<Union>s = i)"
-
-lemma division_ofD[dest]:
- assumes "s division_of i"
- shows "finite s"
- and "\<And>k. k \<in> s \<Longrightarrow> k \<subseteq> i"
- and "\<And>k. k \<in> s \<Longrightarrow> k \<noteq> {}"
- and "\<And>k. k \<in> s \<Longrightarrow> \<exists>a b. k = cbox a b"
- and "\<And>k1 k2. k1 \<in> s \<Longrightarrow> k2 \<in> s \<Longrightarrow> k1 \<noteq> k2 \<Longrightarrow> interior(k1) \<inter> interior(k2) = {}"
- and "\<Union>s = i"
- using assms unfolding division_of_def by auto
-
-lemma division_ofI:
- assumes "finite s"
- and "\<And>k. k \<in> s \<Longrightarrow> k \<subseteq> i"
- and "\<And>k. k \<in> s \<Longrightarrow> k \<noteq> {}"
- and "\<And>k. k \<in> s \<Longrightarrow> \<exists>a b. k = cbox a b"
- and "\<And>k1 k2. k1 \<in> s \<Longrightarrow> k2 \<in> s \<Longrightarrow> k1 \<noteq> k2 \<Longrightarrow> interior k1 \<inter> interior k2 = {}"
- and "\<Union>s = i"
- shows "s division_of i"
- using assms unfolding division_of_def by auto
-
-lemma division_of_finite: "s division_of i \<Longrightarrow> finite s"
- unfolding division_of_def by auto
-
-lemma division_of_self[intro]: "cbox a b \<noteq> {} \<Longrightarrow> {cbox a b} division_of (cbox a b)"
- unfolding division_of_def by auto
-
-lemma division_of_trivial[simp]: "s division_of {} \<longleftrightarrow> s = {}"
- unfolding division_of_def by auto
-
-lemma division_of_sing[simp]:
- "s division_of cbox a (a::'a::euclidean_space) \<longleftrightarrow> s = {cbox a a}"
- (is "?l = ?r")
-proof
- assume ?r
- moreover
- { fix k
- assume "s = {{a}}" "k\<in>s"
- then have "\<exists>x y. k = cbox x y"
- apply (rule_tac x=a in exI)+
- apply (force simp: cbox_sing)
- done
- }
- ultimately show ?l
- unfolding division_of_def cbox_sing by auto
-next
- assume ?l
- note * = conjunctD4[OF this[unfolded division_of_def cbox_sing]]
- {
- fix x
- assume x: "x \<in> s" have "x = {a}"
- using *(2)[rule_format,OF x] by auto
- }
- moreover have "s \<noteq> {}"
- using *(4) by auto
- ultimately show ?r
- unfolding cbox_sing by auto
-qed
-
-lemma elementary_empty: obtains p where "p division_of {}"
- unfolding division_of_trivial by auto
-
-lemma elementary_interval: obtains p where "p division_of (cbox a b)"
- by (metis division_of_trivial division_of_self)
-
-lemma division_contains: "s division_of i \<Longrightarrow> \<forall>x\<in>i. \<exists>k\<in>s. x \<in> k"
- unfolding division_of_def by auto
-
-lemma forall_in_division:
- "d division_of i \<Longrightarrow> (\<forall>x\<in>d. P x) \<longleftrightarrow> (\<forall>a b. cbox a b \<in> d \<longrightarrow> P (cbox a b))"
- unfolding division_of_def by fastforce
-
-lemma division_of_subset:
- assumes "p division_of (\<Union>p)"
- and "q \<subseteq> p"
- shows "q division_of (\<Union>q)"
-proof (rule division_ofI)
- note * = division_ofD[OF assms(1)]
- show "finite q"
- using "*"(1) assms(2) infinite_super by auto
- {
- fix k
- assume "k \<in> q"
- then have kp: "k \<in> p"
- using assms(2) by auto
- show "k \<subseteq> \<Union>q"
- using \<open>k \<in> q\<close> by auto
- show "\<exists>a b. k = cbox a b"
- using *(4)[OF kp] by auto
- show "k \<noteq> {}"
- using *(3)[OF kp] by auto
- }
- fix k1 k2
- assume "k1 \<in> q" "k2 \<in> q" "k1 \<noteq> k2"
- then have **: "k1 \<in> p" "k2 \<in> p" "k1 \<noteq> k2"
- using assms(2) by auto
- show "interior k1 \<inter> interior k2 = {}"
- using *(5)[OF **] by auto
-qed auto
-
-lemma division_of_union_self[intro]: "p division_of s \<Longrightarrow> p division_of (\<Union>p)"
- unfolding division_of_def by auto
-
lemma division_of_content_0:
assumes "content (cbox a b) = 0" "d division_of (cbox a b)"
shows "\<forall>k\<in>d. content k = 0"
unfolding forall_in_division[OF assms(2)]
by (metis antisym_conv assms content_pos_le content_subset division_ofD(2))
-lemma division_inter:
- fixes s1 s2 :: "'a::euclidean_space set"
- assumes "p1 division_of s1"
- and "p2 division_of s2"
- shows "{k1 \<inter> k2 | k1 k2. k1 \<in> p1 \<and> k2 \<in> p2 \<and> k1 \<inter> k2 \<noteq> {}} division_of (s1 \<inter> s2)"
- (is "?A' division_of _")
-proof -
- let ?A = "{s. s \<in> (\<lambda>(k1,k2). k1 \<inter> k2) ` (p1 \<times> p2) \<and> s \<noteq> {}}"
- have *: "?A' = ?A" by auto
- show ?thesis
- unfolding *
- proof (rule division_ofI)
- have "?A \<subseteq> (\<lambda>(x, y). x \<inter> y) ` (p1 \<times> p2)"
- by auto
- moreover have "finite (p1 \<times> p2)"
- using assms unfolding division_of_def by auto
- ultimately show "finite ?A" by auto
- have *: "\<And>s. \<Union>{x\<in>s. x \<noteq> {}} = \<Union>s"
- by auto
- show "\<Union>?A = s1 \<inter> s2"
- apply (rule set_eqI)
- unfolding * and UN_iff
- using division_ofD(6)[OF assms(1)] and division_ofD(6)[OF assms(2)]
- apply auto
- done
- {
- fix k
- assume "k \<in> ?A"
- then obtain k1 k2 where k: "k = k1 \<inter> k2" "k1 \<in> p1" "k2 \<in> p2" "k \<noteq> {}"
- by auto
- then show "k \<noteq> {}"
- by auto
- show "k \<subseteq> s1 \<inter> s2"
- using division_ofD(2)[OF assms(1) k(2)] and division_ofD(2)[OF assms(2) k(3)]
- unfolding k by auto
- obtain a1 b1 where k1: "k1 = cbox a1 b1"
- using division_ofD(4)[OF assms(1) k(2)] by blast
- obtain a2 b2 where k2: "k2 = cbox a2 b2"
- using division_ofD(4)[OF assms(2) k(3)] by blast
- show "\<exists>a b. k = cbox a b"
- unfolding k k1 k2 unfolding Int_interval by auto
- }
- fix k1 k2
- assume "k1 \<in> ?A"
- then obtain x1 y1 where k1: "k1 = x1 \<inter> y1" "x1 \<in> p1" "y1 \<in> p2" "k1 \<noteq> {}"
- by auto
- assume "k2 \<in> ?A"
- then obtain x2 y2 where k2: "k2 = x2 \<inter> y2" "x2 \<in> p1" "y2 \<in> p2" "k2 \<noteq> {}"
- by auto
- assume "k1 \<noteq> k2"
- then have th: "x1 \<noteq> x2 \<or> y1 \<noteq> y2"
- unfolding k1 k2 by auto
- have *: "interior x1 \<inter> interior x2 = {} \<or> interior y1 \<inter> interior y2 = {} \<Longrightarrow>
- interior (x1 \<inter> y1) \<subseteq> interior x1 \<Longrightarrow> interior (x1 \<inter> y1) \<subseteq> interior y1 \<Longrightarrow>
- interior (x2 \<inter> y2) \<subseteq> interior x2 \<Longrightarrow> interior (x2 \<inter> y2) \<subseteq> interior y2 \<Longrightarrow>
- interior (x1 \<inter> y1) \<inter> interior (x2 \<inter> y2) = {}" by auto
- show "interior k1 \<inter> interior k2 = {}"
- unfolding k1 k2
- apply (rule *)
- using assms division_ofD(5) k1 k2(2) k2(3) th apply auto
- done
- qed
-qed
-
-lemma division_inter_1:
- assumes "d division_of i"
- and "cbox a (b::'a::euclidean_space) \<subseteq> i"
- shows "{cbox a b \<inter> k | k. k \<in> d \<and> cbox a b \<inter> k \<noteq> {}} division_of (cbox a b)"
-proof (cases "cbox a b = {}")
- case True
- show ?thesis
- unfolding True and division_of_trivial by auto
-next
- case False
- have *: "cbox a b \<inter> i = cbox a b" using assms(2) by auto
- show ?thesis
- using division_inter[OF division_of_self[OF False] assms(1)]
- unfolding * by auto
-qed
-
-lemma elementary_inter:
- fixes s t :: "'a::euclidean_space set"
- assumes "p1 division_of s"
- and "p2 division_of t"
- shows "\<exists>p. p division_of (s \<inter> t)"
-using assms division_inter by blast
-
-lemma elementary_inters:
- assumes "finite f"
- and "f \<noteq> {}"
- and "\<forall>s\<in>f. \<exists>p. p division_of (s::('a::euclidean_space) set)"
- shows "\<exists>p. p division_of (\<Inter>f)"
- using assms
-proof (induct f rule: finite_induct)
- case (insert x f)
- show ?case
- proof (cases "f = {}")
- case True
- then show ?thesis
- unfolding True using insert by auto
- next
- case False
- obtain p where "p division_of \<Inter>f"
- using insert(3)[OF False insert(5)[unfolded ball_simps,THEN conjunct2]] ..
- moreover obtain px where "px division_of x"
- using insert(5)[rule_format,OF insertI1] ..
- ultimately show ?thesis
- by (simp add: elementary_inter Inter_insert)
- qed
-qed auto
-
-lemma division_disjoint_union:
- assumes "p1 division_of s1"
- and "p2 division_of s2"
- and "interior s1 \<inter> interior s2 = {}"
- shows "(p1 \<union> p2) division_of (s1 \<union> s2)"
-proof (rule division_ofI)
- note d1 = division_ofD[OF assms(1)]
- note d2 = division_ofD[OF assms(2)]
- show "finite (p1 \<union> p2)"
- using d1(1) d2(1) by auto
- show "\<Union>(p1 \<union> p2) = s1 \<union> s2"
- using d1(6) d2(6) by auto
- {
- fix k1 k2
- assume as: "k1 \<in> p1 \<union> p2" "k2 \<in> p1 \<union> p2" "k1 \<noteq> k2"
- moreover
- let ?g="interior k1 \<inter> interior k2 = {}"
- {
- assume as: "k1\<in>p1" "k2\<in>p2"
- have ?g
- using interior_mono[OF d1(2)[OF as(1)]] interior_mono[OF d2(2)[OF as(2)]]
- using assms(3) by blast
- }
- moreover
- {
- assume as: "k1\<in>p2" "k2\<in>p1"
- have ?g
- using interior_mono[OF d1(2)[OF as(2)]] interior_mono[OF d2(2)[OF as(1)]]
- using assms(3) by blast
- }
- ultimately show ?g
- using d1(5)[OF _ _ as(3)] and d2(5)[OF _ _ as(3)] by auto
- }
- fix k
- assume k: "k \<in> p1 \<union> p2"
- show "k \<subseteq> s1 \<union> s2"
- using k d1(2) d2(2) by auto
- show "k \<noteq> {}"
- using k d1(3) d2(3) by auto
- show "\<exists>a b. k = cbox a b"
- using k d1(4) d2(4) by auto
-qed
-
-lemma partial_division_extend_1:
- fixes a b c d :: "'a::euclidean_space"
- assumes incl: "cbox c d \<subseteq> cbox a b"
- and nonempty: "cbox c d \<noteq> {}"
- obtains p where "p division_of (cbox a b)" "cbox c d \<in> p"
-proof
- let ?B = "\<lambda>f::'a\<Rightarrow>'a \<times> 'a.
- cbox (\<Sum>i\<in>Basis. (fst (f i) \<bullet> i) *\<^sub>R i) (\<Sum>i\<in>Basis. (snd (f i) \<bullet> i) *\<^sub>R i)"
- define p where "p = ?B ` (Basis \<rightarrow>\<^sub>E {(a, c), (c, d), (d, b)})"
-
- show "cbox c d \<in> p"
- unfolding p_def
- by (auto simp add: box_eq_empty cbox_def intro!: image_eqI[where x="\<lambda>(i::'a)\<in>Basis. (c, d)"])
- {
- fix i :: 'a
- assume "i \<in> Basis"
- with incl nonempty have "a \<bullet> i \<le> c \<bullet> i" "c \<bullet> i \<le> d \<bullet> i" "d \<bullet> i \<le> b \<bullet> i"
- unfolding box_eq_empty subset_box by (auto simp: not_le)
- }
- note ord = this
-
- show "p division_of (cbox a b)"
- proof (rule division_ofI)
- show "finite p"
- unfolding p_def by (auto intro!: finite_PiE)
- {
- fix k
- assume "k \<in> p"
- then obtain f where f: "f \<in> Basis \<rightarrow>\<^sub>E {(a, c), (c, d), (d, b)}" and k: "k = ?B f"
- by (auto simp: p_def)
- then show "\<exists>a b. k = cbox a b"
- by auto
- have "k \<subseteq> cbox a b \<and> k \<noteq> {}"
- proof (simp add: k box_eq_empty subset_box not_less, safe)
- fix i :: 'a
- assume i: "i \<in> Basis"
- with f have "f i = (a, c) \<or> f i = (c, d) \<or> f i = (d, b)"
- by (auto simp: PiE_iff)
- with i ord[of i]
- show "a \<bullet> i \<le> fst (f i) \<bullet> i" "snd (f i) \<bullet> i \<le> b \<bullet> i" "fst (f i) \<bullet> i \<le> snd (f i) \<bullet> i"
- by auto
- qed
- then show "k \<noteq> {}" "k \<subseteq> cbox a b"
- by auto
- {
- fix l
- assume "l \<in> p"
- then obtain g where g: "g \<in> Basis \<rightarrow>\<^sub>E {(a, c), (c, d), (d, b)}" and l: "l = ?B g"
- by (auto simp: p_def)
- assume "l \<noteq> k"
- have "\<exists>i\<in>Basis. f i \<noteq> g i"
- proof (rule ccontr)
- assume "\<not> ?thesis"
- with f g have "f = g"
- by (auto simp: PiE_iff extensional_def intro!: ext)
- with \<open>l \<noteq> k\<close> show False
- by (simp add: l k)
- qed
- then obtain i where *: "i \<in> Basis" "f i \<noteq> g i" ..
- then have "f i = (a, c) \<or> f i = (c, d) \<or> f i = (d, b)"
- "g i = (a, c) \<or> g i = (c, d) \<or> g i = (d, b)"
- using f g by (auto simp: PiE_iff)
- with * ord[of i] show "interior l \<inter> interior k = {}"
- by (auto simp add: l k interior_cbox disjoint_interval intro!: bexI[of _ i])
- }
- note \<open>k \<subseteq> cbox a b\<close>
- }
- moreover
- {
- fix x assume x: "x \<in> cbox a b"
- have "\<forall>i\<in>Basis. \<exists>l. x \<bullet> i \<in> {fst l \<bullet> i .. snd l \<bullet> i} \<and> l \<in> {(a, c), (c, d), (d, b)}"
- proof
- fix i :: 'a
- assume "i \<in> Basis"
- with x ord[of i]
- have "(a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> c \<bullet> i) \<or> (c \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> d \<bullet> i) \<or>
- (d \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i)"
- by (auto simp: cbox_def)
- then show "\<exists>l. x \<bullet> i \<in> {fst l \<bullet> i .. snd l \<bullet> i} \<and> l \<in> {(a, c), (c, d), (d, b)}"
- by auto
- qed
- then obtain f where
- f: "\<forall>i\<in>Basis. x \<bullet> i \<in> {fst (f i) \<bullet> i..snd (f i) \<bullet> i} \<and> f i \<in> {(a, c), (c, d), (d, b)}"
- unfolding bchoice_iff ..
- moreover from f have "restrict f Basis \<in> Basis \<rightarrow>\<^sub>E {(a, c), (c, d), (d, b)}"
- by auto
- moreover from f have "x \<in> ?B (restrict f Basis)"
- by (auto simp: mem_box)
- ultimately have "\<exists>k\<in>p. x \<in> k"
- unfolding p_def by blast
- }
- ultimately show "\<Union>p = cbox a b"
- by auto
- qed
-qed
-
-lemma partial_division_extend_interval:
- assumes "p division_of (\<Union>p)" "(\<Union>p) \<subseteq> cbox a b"
- obtains q where "p \<subseteq> q" "q division_of cbox a (b::'a::euclidean_space)"
-proof (cases "p = {}")
- case True
- obtain q where "q division_of (cbox a b)"
- by (rule elementary_interval)
- then show ?thesis
- using True that by blast
-next
- case False
- note p = division_ofD[OF assms(1)]
- have div_cbox: "\<forall>k\<in>p. \<exists>q. q division_of cbox a b \<and> k \<in> q"
- proof
- fix k
- assume kp: "k \<in> p"
- obtain c d where k: "k = cbox c d"
- using p(4)[OF kp] by blast
- have *: "cbox c d \<subseteq> cbox a b" "cbox c d \<noteq> {}"
- using p(2,3)[OF kp, unfolded k] using assms(2)
- by (blast intro: order.trans)+
- obtain q where "q division_of cbox a b" "cbox c d \<in> q"
- by (rule partial_division_extend_1[OF *])
- then show "\<exists>q. q division_of cbox a b \<and> k \<in> q"
- unfolding k by auto
- qed
- obtain q where q: "\<And>x. x \<in> p \<Longrightarrow> q x division_of cbox a b" "\<And>x. x \<in> p \<Longrightarrow> x \<in> q x"
- using bchoice[OF div_cbox] by blast
- { fix x
- assume x: "x \<in> p"
- have "q x division_of \<Union>q x"
- apply (rule division_ofI)
- using division_ofD[OF q(1)[OF x]]
- apply auto
- done }
- then have "\<And>x. x \<in> p \<Longrightarrow> \<exists>d. d division_of \<Union>(q x - {x})"
- by (meson Diff_subset division_of_subset)
- then have "\<exists>d. d division_of \<Inter>((\<lambda>i. \<Union>(q i - {i})) ` p)"
- apply -
- apply (rule elementary_inters [OF finite_imageI[OF p(1)]])
- apply (auto simp: False elementary_inters [OF finite_imageI[OF p(1)]])
- done
- then obtain d where d: "d division_of \<Inter>((\<lambda>i. \<Union>(q i - {i})) ` p)" ..
- have "d \<union> p division_of cbox a b"
- proof -
- have te: "\<And>s f t. s \<noteq> {} \<Longrightarrow> \<forall>i\<in>s. f i \<union> i = t \<Longrightarrow> t = \<Inter>(f ` s) \<union> \<Union>s" by auto
- have cbox_eq: "cbox a b = \<Inter>((\<lambda>i. \<Union>(q i - {i})) ` p) \<union> \<Union>p"
- proof (rule te[OF False], clarify)
- fix i
- assume i: "i \<in> p"
- show "\<Union>(q i - {i}) \<union> i = cbox a b"
- using division_ofD(6)[OF q(1)[OF i]] using q(2)[OF i] by auto
- qed
- { fix k
- assume k: "k \<in> p"
- have *: "\<And>u t s. t \<inter> s = {} \<Longrightarrow> u \<subseteq> s \<Longrightarrow> u \<inter> t = {}"
- by auto
- have "interior (\<Inter>i\<in>p. \<Union>(q i - {i})) \<inter> interior k = {}"
- proof (rule *[OF inter_interior_unions_intervals])
- note qk=division_ofD[OF q(1)[OF k]]
- show "finite (q k - {k})" "open (interior k)" "\<forall>t\<in>q k - {k}. \<exists>a b. t = cbox a b"
- using qk by auto
- show "\<forall>t\<in>q k - {k}. interior k \<inter> interior t = {}"
- using qk(5) using q(2)[OF k] by auto
- show "interior (\<Inter>i\<in>p. \<Union>(q i - {i})) \<subseteq> interior (\<Union>(q k - {k}))"
- apply (rule interior_mono)+
- using k
- apply auto
- done
- qed } note [simp] = this
- show "d \<union> p division_of (cbox a b)"
- unfolding cbox_eq
- apply (rule division_disjoint_union[OF d assms(1)])
- apply (rule inter_interior_unions_intervals)
- apply (rule p open_interior ballI)+
- apply simp_all
- done
- qed
- then show ?thesis
- by (meson Un_upper2 that)
-qed
-
-lemma elementary_bounded[dest]:
- fixes s :: "'a::euclidean_space set"
- shows "p division_of s \<Longrightarrow> bounded s"
- unfolding division_of_def by (metis bounded_Union bounded_cbox)
-
-lemma elementary_subset_cbox:
- "p division_of s \<Longrightarrow> \<exists>a b. s \<subseteq> cbox a (b::'a::euclidean_space)"
- by (meson elementary_bounded bounded_subset_cbox)
-
-lemma division_union_intervals_exists:
- fixes a b :: "'a::euclidean_space"
- assumes "cbox a b \<noteq> {}"
- obtains p where "(insert (cbox a b) p) division_of (cbox a b \<union> cbox c d)"
-proof (cases "cbox c d = {}")
- case True
- show ?thesis
- apply (rule that[of "{}"])
- unfolding True
- using assms
- apply auto
- done
-next
- case False
- show ?thesis
- proof (cases "cbox a b \<inter> cbox c d = {}")
- case True
- then show ?thesis
- by (metis that False assms division_disjoint_union division_of_self insert_is_Un interior_Int interior_empty)
- next
- case False
- obtain u v where uv: "cbox a b \<inter> cbox c d = cbox u v"
- unfolding Int_interval by auto
- have uv_sub: "cbox u v \<subseteq> cbox c d" using uv by auto
- obtain p where "p division_of cbox c d" "cbox u v \<in> p"
- by (rule partial_division_extend_1[OF uv_sub False[unfolded uv]])
- note p = this division_ofD[OF this(1)]
- have "interior (cbox a b \<inter> \<Union>(p - {cbox u v})) = interior(cbox u v \<inter> \<Union>(p - {cbox u v}))"
- apply (rule arg_cong[of _ _ interior])
- using p(8) uv by auto
- also have "\<dots> = {}"
- unfolding interior_Int
- apply (rule inter_interior_unions_intervals)
- using p(6) p(7)[OF p(2)] p(3)
- apply auto
- done
- finally have [simp]: "interior (cbox a b) \<inter> interior (\<Union>(p - {cbox u v})) = {}" by simp
- have cbe: "cbox a b \<union> cbox c d = cbox a b \<union> \<Union>(p - {cbox u v})"
- using p(8) unfolding uv[symmetric] by auto
- have "insert (cbox a b) (p - {cbox u v}) division_of cbox a b \<union> \<Union>(p - {cbox u v})"
- proof -
- have "{cbox a b} division_of cbox a b"
- by (simp add: assms division_of_self)
- then show "insert (cbox a b) (p - {cbox u v}) division_of cbox a b \<union> \<Union>(p - {cbox u v})"
- by (metis (no_types) Diff_subset \<open>interior (cbox a b) \<inter> interior (\<Union>(p - {cbox u v})) = {}\<close> division_disjoint_union division_of_subset insert_is_Un p(1) p(8))
- qed
- with that[of "p - {cbox u v}"] show ?thesis by (simp add: cbe)
- qed
-qed
-
-lemma division_of_unions:
- assumes "finite f"
- and "\<And>p. p \<in> f \<Longrightarrow> p division_of (\<Union>p)"
- and "\<And>k1 k2. k1 \<in> \<Union>f \<Longrightarrow> k2 \<in> \<Union>f \<Longrightarrow> k1 \<noteq> k2 \<Longrightarrow> interior k1 \<inter> interior k2 = {}"
- shows "\<Union>f division_of \<Union>\<Union>f"
- using assms
- by (auto intro!: division_ofI)
-
-lemma elementary_union_interval:
- fixes a b :: "'a::euclidean_space"
- assumes "p division_of \<Union>p"
- obtains q where "q division_of (cbox a b \<union> \<Union>p)"
-proof -
- note assm = division_ofD[OF assms]
- have lem1: "\<And>f s. \<Union>\<Union>(f ` s) = \<Union>((\<lambda>x. \<Union>(f x)) ` s)"
- by auto
- have lem2: "\<And>f s. f \<noteq> {} \<Longrightarrow> \<Union>{s \<union> t |t. t \<in> f} = s \<union> \<Union>f"
+lemma setsum_content_null:
+ assumes "content (cbox a b) = 0"
+ and "p tagged_division_of (cbox a b)"
+ shows "setsum (\<lambda>(x,k). content k *\<^sub>R f x) p = (0::'a::real_normed_vector)"
+proof (rule setsum.neutral, rule)
+ fix y
+ assume y: "y \<in> p"
+ obtain x k where xk: "y = (x, k)"
+ using surj_pair[of y] by blast
+ note assm = tagged_division_ofD(3-4)[OF assms(2) y[unfolded xk]]
+ from this(2) obtain c d where k: "k = cbox c d" by blast
+ have "(\<lambda>(x, k). content k *\<^sub>R f x) y = content k *\<^sub>R f x"
+ unfolding xk by auto
+ also have "\<dots> = 0"
+ using content_subset[OF assm(1)[unfolded k]] content_pos_le[of c d]
+ unfolding assms(1) k
by auto
- {
- presume "p = {} \<Longrightarrow> thesis"
- "cbox a b = {} \<Longrightarrow> thesis"
- "cbox a b \<noteq> {} \<Longrightarrow> interior (cbox a b) = {} \<Longrightarrow> thesis"
- "p \<noteq> {} \<Longrightarrow> interior (cbox a b)\<noteq>{} \<Longrightarrow> cbox a b \<noteq> {} \<Longrightarrow> thesis"
- then show thesis by auto
- next
- assume as: "p = {}"
- obtain p where "p division_of (cbox a b)"
- by (rule elementary_interval)
- then show thesis
- using as that by auto
- next
- assume as: "cbox a b = {}"
- show thesis
- using as assms that by auto
- next
- assume as: "interior (cbox a b) = {}" "cbox a b \<noteq> {}"
- show thesis
- apply (rule that[of "insert (cbox a b) p"],rule division_ofI)
- unfolding finite_insert
- apply (rule assm(1)) unfolding Union_insert
- using assm(2-4) as
- apply -
- apply (fast dest: assm(5))+
- done
- next
- assume as: "p \<noteq> {}" "interior (cbox a b) \<noteq> {}" "cbox a b \<noteq> {}"
- have "\<forall>k\<in>p. \<exists>q. (insert (cbox a b) q) division_of (cbox a b \<union> k)"
- proof
- fix k
- assume kp: "k \<in> p"
- from assm(4)[OF kp] obtain c d where "k = cbox c d" by blast
- then show "\<exists>q. (insert (cbox a b) q) division_of (cbox a b \<union> k)"
- by (meson as(3) division_union_intervals_exists)
- qed
- from bchoice[OF this] obtain q where "\<forall>x\<in>p. insert (cbox a b) (q x) division_of (cbox a b) \<union> x" ..
- note q = division_ofD[OF this[rule_format]]
- let ?D = "\<Union>{insert (cbox a b) (q k) | k. k \<in> p}"
- show thesis
- proof (rule that[OF division_ofI])
- have *: "{insert (cbox a b) (q k) |k. k \<in> p} = (\<lambda>k. insert (cbox a b) (q k)) ` p"
- by auto
- show "finite ?D"
- using "*" assm(1) q(1) by auto
- show "\<Union>?D = cbox a b \<union> \<Union>p"
- unfolding * lem1
- unfolding lem2[OF as(1), of "cbox a b", symmetric]
- using q(6)
- by auto
- fix k
- assume k: "k \<in> ?D"
- then show "k \<subseteq> cbox a b \<union> \<Union>p"
- using q(2) by auto
- show "k \<noteq> {}"
- using q(3) k by auto
- show "\<exists>a b. k = cbox a b"
- using q(4) k by auto
- fix k'
- assume k': "k' \<in> ?D" "k \<noteq> k'"
- obtain x where x: "k \<in> insert (cbox a b) (q x)" "x\<in>p"
- using k by auto
- obtain x' where x': "k'\<in>insert (cbox a b) (q x')" "x'\<in>p"
- using k' by auto
- show "interior k \<inter> interior k' = {}"
- proof (cases "x = x'")
- case True
- show ?thesis
- using True k' q(5) x' x by auto
- next
- case False
- {
- presume "k = cbox a b \<Longrightarrow> ?thesis"
- and "k' = cbox a b \<Longrightarrow> ?thesis"
- and "k \<noteq> cbox a b \<Longrightarrow> k' \<noteq> cbox a b \<Longrightarrow> ?thesis"
- then show ?thesis by linarith
- next
- assume as': "k = cbox a b"
- show ?thesis
- using as' k' q(5) x' by blast
- next
- assume as': "k' = cbox a b"
- show ?thesis
- using as' k'(2) q(5) x by blast
- }
- assume as': "k \<noteq> cbox a b" "k' \<noteq> cbox a b"
- obtain c d where k: "k = cbox c d"
- using q(4)[OF x(2,1)] by blast
- have "interior k \<inter> interior (cbox a b) = {}"
- using as' k'(2) q(5) x by blast
- then have "interior k \<subseteq> interior x"
- using interior_subset_union_intervals
- by (metis as(2) k q(2) x interior_subset_union_intervals)
- moreover
- obtain c d where c_d: "k' = cbox c d"
- using q(4)[OF x'(2,1)] by blast
- have "interior k' \<inter> interior (cbox a b) = {}"
- using as'(2) q(5) x' by blast
- then have "interior k' \<subseteq> interior x'"
- by (metis as(2) c_d interior_subset_union_intervals q(2) x'(1) x'(2))
- ultimately show ?thesis
- using assm(5)[OF x(2) x'(2) False] by auto
- qed
- qed
- }
-qed
-
-lemma elementary_unions_intervals:
- assumes fin: "finite f"
- and "\<And>s. s \<in> f \<Longrightarrow> \<exists>a b. s = cbox a (b::'a::euclidean_space)"
- obtains p where "p division_of (\<Union>f)"
-proof -
- have "\<exists>p. p division_of (\<Union>f)"
- proof (induct_tac f rule:finite_subset_induct)
- show "\<exists>p. p division_of \<Union>{}" using elementary_empty by auto
- next
- fix x F
- assume as: "finite F" "x \<notin> F" "\<exists>p. p division_of \<Union>F" "x\<in>f"
- from this(3) obtain p where p: "p division_of \<Union>F" ..
- from assms(2)[OF as(4)] obtain a b where x: "x = cbox a b" by blast
- have *: "\<Union>F = \<Union>p"
- using division_ofD[OF p] by auto
- show "\<exists>p. p division_of \<Union>insert x F"
- using elementary_union_interval[OF p[unfolded *], of a b]
- unfolding Union_insert x * by metis
- qed (insert assms, auto)
- then show ?thesis
- using that by auto
-qed
-
-lemma elementary_union:
- fixes s t :: "'a::euclidean_space set"
- assumes "ps division_of s" "pt division_of t"
- obtains p where "p division_of (s \<union> t)"
-proof -
- have *: "s \<union> t = \<Union>ps \<union> \<Union>pt"
- using assms unfolding division_of_def by auto
- show ?thesis
- apply (rule elementary_unions_intervals[of "ps \<union> pt"])
- using assms apply auto
- by (simp add: * that)
-qed
-
-lemma partial_division_extend:
- fixes t :: "'a::euclidean_space set"
- assumes "p division_of s"
- and "q division_of t"
- and "s \<subseteq> t"
- obtains r where "p \<subseteq> r" and "r division_of t"
-proof -
- note divp = division_ofD[OF assms(1)] and divq = division_ofD[OF assms(2)]
- obtain a b where ab: "t \<subseteq> cbox a b"
- using elementary_subset_cbox[OF assms(2)] by auto
- obtain r1 where "p \<subseteq> r1" "r1 division_of (cbox a b)"
- using assms
- by (metis ab dual_order.trans partial_division_extend_interval divp(6))