# HG changeset patch # User wenzelm # Date 1498160937 -7200 # Node ID cad55bc7e37ddcaec63d5a75ef6edbc4a055ac93 # Parent 48cfbccaf3f459ac3782e37959a01a9106834e4e# Parent 8cfa8c7ee1f6c80dda2fd9fdbe7c1285bd7c6ed8 merged diff -r 8cfa8c7ee1f6 -r cad55bc7e37d src/HOL/Analysis/Borel_Space.thy --- a/src/HOL/Analysis/Borel_Space.thy Thu Jun 22 21:44:15 2017 +0200 +++ b/src/HOL/Analysis/Borel_Space.thy Thu Jun 22 21:48:57 2017 +0200 @@ -1379,6 +1379,13 @@ shows "(\x. f x *\<^sub>R g x) \ borel_measurable M" using f g by (rule borel_measurable_continuous_Pair) (intro continuous_intros) +lemma borel_measurable_uminus_eq [simp]: + fixes f :: "'a \ 'b::{second_countable_topology, real_normed_vector}" + shows "(\x. - f x) \ borel_measurable M \ f \ borel_measurable M" (is "?l = ?r") +proof + assume ?l from borel_measurable_uminus[OF this] show ?r by simp +qed auto + lemma affine_borel_measurable_vector: fixes f :: "'a \ 'x::real_normed_vector" assumes "f \ borel_measurable M" diff -r 8cfa8c7ee1f6 -r cad55bc7e37d src/HOL/Analysis/Cauchy_Integral_Theorem.thy --- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Thu Jun 22 21:44:15 2017 +0200 +++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Thu Jun 22 21:48:57 2017 +0200 @@ -1341,9 +1341,6 @@ using assms apply (blast intro: has_contour_integral_subpath) done -lemma has_integral_integrable_integral: "(f has_integral i) s \ f integrable_on s \ integral s f = i" - by blast - lemma has_integral_contour_integral_subpath: assumes "f contour_integrable_on g" "valid_path g" "u \ {0..1}" "v \ {0..1}" "u \ v" shows "(((\x. f(g x) * vector_derivative g (at x))) diff -r 8cfa8c7ee1f6 -r cad55bc7e37d src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy --- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Thu Jun 22 21:44:15 2017 +0200 +++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Thu Jun 22 21:48:57 2017 +0200 @@ -860,7 +860,7 @@ then have "(?f has_integral F b - F a) {a .. b}" by (subst has_integral_cong[where g=f]) auto then have "(?f has_integral F b - F a) UNIV" - by (intro has_integral_on_superset[where t=UNIV and s="{a..b}"]) auto + by (intro has_integral_on_superset[where T=UNIV and S="{a..b}"]) auto ultimately show "integral\<^sup>L lborel ?f = F b - F a" by (rule has_integral_unique) qed @@ -908,6 +908,7 @@ (infixr "absolutely'_integrable'_on" 46) where "f absolutely_integrable_on s \ set_integrable lebesgue s f" + lemma absolutely_integrable_on_def: fixes f :: "'a::euclidean_space \ 'b::euclidean_space" shows "f absolutely_integrable_on s \ f integrable_on s \ (\x. norm (f x)) integrable_on s" @@ -933,6 +934,17 @@ by (auto simp: integrable_on_def nn_integral_completion) qed qed + +lemma absolutely_integrable_on_null [intro]: + fixes f :: "'a::euclidean_space \ 'b::euclidean_space" + shows "content (cbox a b) = 0 \ f absolutely_integrable_on (cbox a b)" + by (auto simp: absolutely_integrable_on_def) + +lemma absolutely_integrable_on_open_interval: + fixes f :: "'a :: euclidean_space \ 'b :: euclidean_space" + shows "f absolutely_integrable_on box a b \ + f absolutely_integrable_on cbox a b" + by (auto simp: integrable_on_open_interval absolutely_integrable_on_def) lemma absolutely_integrable_restrict_UNIV: "(\x. if x \ s then f x else 0) absolutely_integrable_on UNIV \ f absolutely_integrable_on s" @@ -2075,7 +2087,7 @@ assumes "f integrable_on UNIV" and "\d. d division_of (\d) \ sum (\k. norm (integral k f)) d \ B" shows "f absolutely_integrable_on UNIV" -proof (rule absolutely_integrable_onI, fact, rule) +proof (rule absolutely_integrable_onI, fact) let ?f = "\d. \k\d. norm (integral k f)" and ?D = "{d. d division_of (\d)}" have D_1: "?D \ {}" by (rule elementary_interval) auto @@ -2091,7 +2103,7 @@ apply (rule assms(2)[rule_format]) apply auto done - show "((\x. norm (f x)) has_integral ?S) UNIV" + have "((\x. norm (f x)) has_integral ?S) UNIV" apply (subst has_integral_alt') apply safe proof goal_cases @@ -2224,6 +2236,8 @@ qed qed (insert K, auto) qed + then show "(\x. norm (f x)) integrable_on UNIV" + by blast qed lemma absolutely_integrable_add[intro]: diff -r 8cfa8c7ee1f6 -r cad55bc7e37d src/HOL/Analysis/Henstock_Kurzweil_Integration.thy --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Thu Jun 22 21:44:15 2017 +0200 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Thu Jun 22 21:48:57 2017 +0200 @@ -273,13 +273,13 @@ definition "integral i f = (SOME y. (f has_integral y) i \ ~ f integrable_on i \ y=0)" -lemma integrable_integral[dest]: "f integrable_on i \ (f has_integral (integral i f)) i" +lemma integrable_integral[intro]: "f integrable_on i \ (f has_integral (integral i f)) i" unfolding integrable_on_def integral_def by (metis (mono_tags, lifting) someI_ex) lemma not_integrable_integral: "~ f integrable_on i \ integral i f = 0" unfolding integrable_on_def integral_def by blast -lemma has_integral_integrable[intro]: "(f has_integral i) s \ f integrable_on s" +lemma has_integral_integrable[dest]: "(f has_integral i) s \ f integrable_on s" unfolding integrable_on_def by auto lemma has_integral_integral: "f integrable_on s \ (f has_integral (integral s f)) s" @@ -358,7 +358,6 @@ apply (rule someI_ex) by blast - lemma has_integral_const [intro]: fixes a b :: "'a::euclidean_space" shows "((\x. c) has_integral (content (cbox a b) *\<^sub>R c)) (cbox a b)" @@ -372,6 +371,9 @@ shows "((\x. c) has_integral (content {a .. b} *\<^sub>R c)) {a .. b}" by (metis box_real(2) has_integral_const) +lemma has_integral_integrable_integral: "(f has_integral i) s \ f integrable_on s \ integral s f = i" + by blast + lemma integral_const [simp]: fixes a b :: "'a::euclidean_space" shows "integral (cbox a b) (\x. c) = content (cbox a b) *\<^sub>R c" @@ -408,17 +410,17 @@ by (subst has_integral_alt) (force simp add: *) qed -lemma has_integral_0[simp]: "((\x::'n::euclidean_space. 0) has_integral 0) s" +lemma has_integral_0[simp]: "((\x::'n::euclidean_space. 0) has_integral 0) S" by (rule has_integral_is_0) auto -lemma has_integral_0_eq[simp]: "((\x. 0) has_integral i) s \ i = 0" +lemma has_integral_0_eq[simp]: "((\x. 0) has_integral i) S \ i = 0" using has_integral_unique[OF has_integral_0] by auto lemma has_integral_linear: fixes f :: "'n::euclidean_space \ 'a::real_normed_vector" - assumes "(f has_integral y) s" + assumes "(f has_integral y) S" and "bounded_linear h" - shows "((h \ f) has_integral ((h y))) s" + shows "((h \ f) has_integral ((h y))) S" proof - interpret bounded_linear h using assms(2) . @@ -427,11 +429,11 @@ have lem: "\a b y f::'n\'a. (f has_integral y) (cbox a b) \ ((h \ f) has_integral h y) (cbox a b)" unfolding has_integral_cbox by (drule tendsto) (simp add: sum scaleR split_beta') { - presume "\ (\a b. s = cbox a b) \ ?thesis" + presume "\ (\a b. S = cbox a b) \ ?thesis" then show ?thesis using assms(1) lem by blast } - assume as: "\ (\a b. s = cbox a b)" + assume as: "\ (\a b. S = cbox a b)" then show ?thesis proof (subst has_integral_alt, clarsimp) fix e :: real @@ -440,17 +442,17 @@ obtain M where M: "M > 0" "\a b. ball 0 M \ cbox a b \ - \z. ((\x. if x \ s then f x else 0) has_integral z) (cbox a b) \ norm (z - y) < e / B" + \z. ((\x. if x \ S then f x else 0) has_integral z) (cbox a b) \ norm (z - y) < e / B" using has_integral_altD[OF assms(1) as *] by blast show "\B>0. \a b. ball 0 B \ cbox a b \ - (\z. ((\x. if x \ s then (h \ f) x else 0) has_integral z) (cbox a b) \ norm (z - h y) < e)" + (\z. ((\x. if x \ S then (h \ f) x else 0) has_integral z) (cbox a b) \ norm (z - h y) < e)" proof (rule_tac x=M in exI, clarsimp simp add: M, goal_cases) case prems: (1 a b) obtain z where z: - "((\x. if x \ s then f x else 0) has_integral z) (cbox a b)" + "((\x. if x \ S then f x else 0) has_integral z) (cbox a b)" "norm (z - y) < e / B" using M(2)[OF prems(1)] by blast - have *: "(\x. if x \ s then (h \ f) x else 0) = h \ (\x. if x \ s then f x else 0)" + have *: "(\x. if x \ S then (h \ f) x else 0) = h \ (\x. if x \ S then f x else 0)" using zero by auto show ?case apply (rule_tac x="h z" in exI) @@ -462,7 +464,7 @@ qed lemma has_integral_scaleR_left: - "(f has_integral y) s \ ((\x. f x *\<^sub>R c) has_integral (y *\<^sub>R c)) s" + "(f has_integral y) S \ ((\x. f x *\<^sub>R c) has_integral (y *\<^sub>R c)) S" using has_integral_linear[OF _ bounded_linear_scaleR_left] by (simp add: comp_def) lemma integrable_on_scaleR_left: @@ -472,27 +474,27 @@ lemma has_integral_mult_left: fixes c :: "_ :: real_normed_algebra" - shows "(f has_integral y) s \ ((\x. f x * c) has_integral (y * c)) s" + shows "(f has_integral y) S \ ((\x. f x * c) has_integral (y * c)) S" using has_integral_linear[OF _ bounded_linear_mult_left] by (simp add: comp_def) -text\The case analysis eliminates the condition @{term "f integrable_on s"} at the cost +text\The case analysis eliminates the condition @{term "f integrable_on S"} at the cost of the type class constraint \division_ring\\ corollary integral_mult_left [simp]: fixes c:: "'a::{real_normed_algebra,division_ring}" - shows "integral s (\x. f x * c) = integral s f * c" -proof (cases "f integrable_on s \ c = 0") + shows "integral S (\x. f x * c) = integral S f * c" +proof (cases "f integrable_on S \ c = 0") case True then show ?thesis by (force intro: has_integral_mult_left) next - case False then have "~ (\x. f x * c) integrable_on s" - using has_integral_mult_left [of "(\x. f x * c)" _ s "inverse c"] - by (force simp add: mult.assoc) + case False then have "~ (\x. f x * c) integrable_on S" + using has_integral_mult_left [of "(\x. f x * c)" _ S "inverse c"] + by (auto simp add: mult.assoc) with False show ?thesis by (simp add: not_integrable_integral) qed corollary integral_mult_right [simp]: fixes c:: "'a::{real_normed_field}" - shows "integral s (\x. c * f x) = c * integral s f" + shows "integral S (\x. c * f x) = c * integral S f" by (simp add: mult.commute [of c]) corollary integral_divide [simp]: @@ -506,7 +508,7 @@ shows "(f has_integral y) i \ ((\x. c * f x) has_integral (c * y)) i" using has_integral_linear[OF _ bounded_linear_mult_right] by (simp add: comp_def) -lemma has_integral_cmul: "(f has_integral k) s \ ((\x. c *\<^sub>R f x) has_integral (c *\<^sub>R k)) s" +lemma has_integral_cmul: "(f has_integral k) S \ ((\x. c *\<^sub>R f x) has_integral (c *\<^sub>R k)) S" unfolding o_def[symmetric] by (metis has_integral_linear bounded_linear_scaleR_right) @@ -523,17 +525,17 @@ unfolding real_scaleR_def . qed -lemma has_integral_neg: "(f has_integral k) s \ ((\x. -(f x)) has_integral -k) s" +lemma has_integral_neg: "(f has_integral k) S \ ((\x. -(f x)) has_integral -k) S" by (drule_tac c="-1" in has_integral_cmul) auto -lemma has_integral_neg_iff: "((\x. - f x) has_integral k) s \ (f has_integral - k) s" +lemma has_integral_neg_iff: "((\x. - f x) has_integral k) S \ (f has_integral - k) S" using has_integral_neg[of f "- k"] has_integral_neg[of "\x. - f x" k] by auto lemma has_integral_add: fixes f :: "'n::euclidean_space \ 'a::real_normed_vector" - assumes "(f has_integral k) s" - and "(g has_integral l) s" - shows "((\x. f x + g x) has_integral (k + l)) s" + assumes "(f has_integral k) S" + and "(g has_integral l) S" + shows "((\x. f x + g x) has_integral (k + l)) S" proof - have lem: "(f has_integral k) (cbox a b) \ (g has_integral l) (cbox a b) \ ((\x. f x + g x) has_integral (k + l)) (cbox a b)" @@ -541,11 +543,11 @@ unfolding has_integral_cbox by (simp add: split_beta' scaleR_add_right sum.distrib[abs_def] tendsto_add) { - presume "\ (\a b. s = cbox a b) \ ?thesis" + presume "\ (\a b. S = cbox a b) \ ?thesis" then show ?thesis using assms lem by force } - assume as: "\ (\a b. s = cbox a b)" + assume as: "\ (\a b. S = cbox a b)" then show ?thesis proof (subst has_integral_alt, clarsimp, goal_cases) case (1 e) @@ -555,13 +557,13 @@ obtain B1 where B1: "0 < B1" "\a b. ball 0 B1 \ cbox a b \ - \z. ((\x. if x \ s then f x else 0) has_integral z) (cbox a b) \ norm (z - k) < e / 2" + \z. ((\x. if x \ S then f x else 0) has_integral z) (cbox a b) \ norm (z - k) < e / 2" by blast from has_integral_altD[OF assms(2) as *] obtain B2 where B2: "0 < B2" "\a b. ball 0 B2 \ (cbox a b) \ - \z. ((\x. if x \ s then g x else 0) has_integral z) (cbox a b) \ norm (z - l) < e / 2" + \z. ((\x. if x \ S then g x else 0) has_integral z) (cbox a b) \ norm (z - l) < e / 2" by blast show ?case proof (rule_tac x="max B1 B2" in exI, clarsimp simp add: max.strict_coboundedI1 B1) @@ -570,17 +572,17 @@ then have *: "ball 0 B1 \ cbox a (b::'n)" "ball 0 B2 \ cbox a (b::'n)" by auto obtain w where w: - "((\x. if x \ s then f x else 0) has_integral w) (cbox a b)" + "((\x. if x \ S then f x else 0) has_integral w) (cbox a b)" "norm (w - k) < e / 2" using B1(2)[OF *(1)] by blast obtain z where z: - "((\x. if x \ s then g x else 0) has_integral z) (cbox a b)" + "((\x. if x \ S then g x else 0) has_integral z) (cbox a b)" "norm (z - l) < e / 2" using B2(2)[OF *(2)] by blast - have *: "\x. (if x \ s then f x + g x else 0) = - (if x \ s then f x else 0) + (if x \ s then g x else 0)" + have *: "\x. (if x \ S then f x + g x else 0) = + (if x \ S then f x else 0) + (if x \ S then g x else 0)" by auto - show "\z. ((\x. if x \ s then f x + g x else 0) has_integral z) (cbox a b) \ norm (z - (k + l)) < e" + show "\z. ((\x. if x \ S then f x + g x else 0) has_integral z) (cbox a b) \ norm (z - (k + l)) < e" apply (rule_tac x="w + z" in exI) apply (simp add: lem[OF w(1) z(1), unfolded *[symmetric]]) using norm_triangle_ineq[of "w - k" "z - l"] w(2) z(2) @@ -591,93 +593,92 @@ qed lemma has_integral_diff: - "(f has_integral k) s \ (g has_integral l) s \ - ((\x. f x - g x) has_integral (k - l)) s" - using has_integral_add[OF _ has_integral_neg, of f k s g l] + "(f has_integral k) S \ (g has_integral l) S \ + ((\x. f x - g x) has_integral (k - l)) S" + using has_integral_add[OF _ has_integral_neg, of f k S g l] by (auto simp: algebra_simps) lemma integral_0 [simp]: - "integral s (\x::'n::euclidean_space. 0::'m::real_normed_vector) = 0" + "integral S (\x::'n::euclidean_space. 0::'m::real_normed_vector) = 0" by (rule integral_unique has_integral_0)+ -lemma integral_add: "f integrable_on s \ g integrable_on s \ - integral s (\x. f x + g x) = integral s f + integral s g" +lemma integral_add: "f integrable_on S \ g integrable_on S \ + integral S (\x. f x + g x) = integral S f + integral S g" by (rule integral_unique) (metis integrable_integral has_integral_add) -lemma integral_cmul [simp]: "integral s (\x. c *\<^sub>R f x) = c *\<^sub>R integral s f" -proof (cases "f integrable_on s \ c = 0") - case True with has_integral_cmul show ?thesis by force +lemma integral_cmul [simp]: "integral S (\x. c *\<^sub>R f x) = c *\<^sub>R integral S f" +proof (cases "f integrable_on S \ c = 0") + case True with has_integral_cmul integrable_integral show ?thesis + by fastforce next - case False then have "~ (\x. c *\<^sub>R f x) integrable_on s" - using has_integral_cmul [of "(\x. c *\<^sub>R f x)" _ s "inverse c"] - by force + case False then have "~ (\x. c *\<^sub>R f x) integrable_on S" + using has_integral_cmul [of "(\x. c *\<^sub>R f x)" _ S "inverse c"] by auto with False show ?thesis by (simp add: not_integrable_integral) qed -lemma integral_neg [simp]: "integral s (\x. - f x) = - integral s f" -proof (cases "f integrable_on s") +lemma integral_neg [simp]: "integral S (\x. - f x) = - integral S f" +proof (cases "f integrable_on S") case True then show ?thesis by (simp add: has_integral_neg integrable_integral integral_unique) next - case False then have "~ (\x. - f x) integrable_on s" - using has_integral_neg [of "(\x. - f x)" _ s ] - by force + case False then have "~ (\x. - f x) integrable_on S" + using has_integral_neg [of "(\x. - f x)" _ S ] by auto with False show ?thesis by (simp add: not_integrable_integral) qed -lemma integral_diff: "f integrable_on s \ g integrable_on s \ - integral s (\x. f x - g x) = integral s f - integral s g" +lemma integral_diff: "f integrable_on S \ g integrable_on S \ + integral S (\x. f x - g x) = integral S f - integral S g" by (rule integral_unique) (metis integrable_integral has_integral_diff) -lemma integrable_0: "(\x. 0) integrable_on s" +lemma integrable_0: "(\x. 0) integrable_on S" unfolding integrable_on_def using has_integral_0 by auto -lemma integrable_add: "f integrable_on s \ g integrable_on s \ (\x. f x + g x) integrable_on s" +lemma integrable_add: "f integrable_on S \ g integrable_on S \ (\x. f x + g x) integrable_on S" unfolding integrable_on_def by(auto intro: has_integral_add) -lemma integrable_cmul: "f integrable_on s \ (\x. c *\<^sub>R f(x)) integrable_on s" +lemma integrable_cmul: "f integrable_on S \ (\x. c *\<^sub>R f(x)) integrable_on S" unfolding integrable_on_def by(auto intro: has_integral_cmul) lemma integrable_on_cmult_iff: fixes c :: real assumes "c \ 0" - shows "(\x. c * f x) integrable_on s \ f integrable_on s" - using integrable_cmul[of "\x. c * f x" s "1 / c"] integrable_cmul[of f s c] \c \ 0\ + shows "(\x. c * f x) integrable_on S \ f integrable_on S" + using integrable_cmul[of "\x. c * f x" S "1 / c"] integrable_cmul[of f S c] \c \ 0\ by auto lemma integrable_on_cmult_left: - assumes "f integrable_on s" - shows "(\x. of_real c * f x) integrable_on s" - using integrable_cmul[of f s "of_real c"] assms + assumes "f integrable_on S" + shows "(\x. of_real c * f x) integrable_on S" + using integrable_cmul[of f S "of_real c"] assms by (simp add: scaleR_conv_of_real) -lemma integrable_neg: "f integrable_on s \ (\x. -f(x)) integrable_on s" +lemma integrable_neg: "f integrable_on S \ (\x. -f(x)) integrable_on S" unfolding integrable_on_def by(auto intro: has_integral_neg) lemma integrable_diff: - "f integrable_on s \ g integrable_on s \ (\x. f x - g x) integrable_on s" + "f integrable_on S \ g integrable_on S \ (\x. f x - g x) integrable_on S" unfolding integrable_on_def by(auto intro: has_integral_diff) lemma integrable_linear: - "f integrable_on s \ bounded_linear h \ (h \ f) integrable_on s" + "f integrable_on S \ bounded_linear h \ (h \ f) integrable_on S" unfolding integrable_on_def by(auto intro: has_integral_linear) lemma integral_linear: - "f integrable_on s \ bounded_linear h \ integral s (h \ f) = h (integral s f)" - apply (rule has_integral_unique [where i=s and f = "h \ f"]) + "f integrable_on S \ bounded_linear h \ integral S (h \ f) = h (integral S f)" + apply (rule has_integral_unique [where i=S and f = "h \ f"]) apply (simp_all add: integrable_integral integrable_linear has_integral_linear ) done lemma integral_component_eq[simp]: fixes f :: "'n::euclidean_space \ 'm::euclidean_space" - assumes "f integrable_on s" - shows "integral s (\x. f x \ k) = integral s f \ k" + assumes "f integrable_on S" + shows "integral S (\x. f x \ k) = integral S f \ k" unfolding integral_linear[OF assms(1) bounded_linear_inner_left,unfolded o_def] .. lemma has_integral_sum: assumes "finite t" - and "\a\t. ((f a) has_integral (i a)) s" - shows "((\x. sum (\a. f a x) t) has_integral (sum i t)) s" + and "\a\t. ((f a) has_integral (i a)) S" + shows "((\x. sum (\a. f a x) t) has_integral (sum i t)) S" using assms(1) subset_refl[of t] proof (induct rule: finite_subset_induct) case empty @@ -689,9 +690,9 @@ qed lemma integral_sum: - "\finite t; \a\t. (f a) integrable_on s\ \ - integral s (\x. sum (\a. f a x) t) = sum (\a. integral s (f a)) t" - by (auto intro: has_integral_sum integrable_integral) + "\finite I; \a. a \ I \ f a integrable_on S\ \ + integral S (\x. \a\I. f a x) = (\a\I. integral S (f a))" + by (simp add: has_integral_sum integrable_integral integral_unique) lemma integrable_sum: "\finite I; \a. a \ I \ f a integrable_on S\ \ (\x. \a\I. f a x) integrable_on S" @@ -927,7 +928,7 @@ by auto from choice[OF this] guess d .. note d=conjunctD2[OF this[rule_format],rule_format] have "\n. gauge (\x. \{d i x |i. i \ {0..n}})" - apply (rule gauge_inters) + apply (rule gauge_Inter) using d(1) apply auto done @@ -993,33 +994,33 @@ subsection \Additivity of integral on abutting intervals.\ lemma tagged_division_split_left_inj_content: - assumes d: "d tagged_division_of i" - and "(x1, k1) \ d" "(x2, k2) \ d" "k1 \ k2" "k1 \ {x. x\k \ c} = k2 \ {x. x\k \ c}" "k \ Basis" - shows "content (k1 \ {x. x\k \ c}) = 0" + assumes \: "\ tagged_division_of S" + and "(x1, K1) \ \" "(x2, K2) \ \" "K1 \ K2" "K1 \ {x. x\k \ c} = K2 \ {x. x\k \ c}" "k \ Basis" + shows "content (K1 \ {x. x\k \ c}) = 0" proof - - from tagged_division_ofD(4)[OF d \(x1, k1) \ d\] obtain a b where k1: "k1 = cbox a b" + from tagged_division_ofD(4)[OF \ \(x1, K1) \ \\] obtain a b where K1: "K1 = cbox a b" by auto - show ?thesis - unfolding k1 interval_split[OF \k \ Basis\] - unfolding content_eq_0_interior - unfolding interval_split[OF \k \ Basis\, symmetric] k1[symmetric] + then have "interior (K1 \ {x. x \ k \ c}) = {}" by (metis tagged_division_split_left_inj assms) + then show ?thesis + unfolding K1 interval_split[OF \