# HG changeset patch # User huffman # Date 1313954551 25200 # Node ID 5daa55003649c6be30b12b698698204458216c5c # Parent 75ec83d45303dbb57c5682c4e02a3d8002c5f94c add lemmas interior_Times and closure_Times diff -r 75ec83d45303 -r 5daa55003649 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Sun Aug 21 11:03:15 2011 -0700 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Sun Aug 21 12:22:31 2011 -0700 @@ -258,33 +258,8 @@ qed lemma closure_direct_sum: -fixes S :: "('n::real_normed_vector) set" -fixes T :: "('m::real_normed_vector) set" shows "closure (S <*> T) = closure S <*> closure T" -proof- -{ fix x assume "x : closure S <*> closure T" - from this obtain xs xt where xst_def: "xs : closure S & xt : closure T & (xs,xt) = x" by auto - { fix ee assume ee_def: "(ee :: real) > 0" - def e == "ee/2" hence e_def: "(e :: real)>0 & 2*e=ee" using ee_def by auto - from this obtain e where e_def: "(e :: real)>0 & 2*e=ee" by auto - obtain ys where ys_def: "ys : S & (dist ys xs < e)" - using e_def xst_def closure_approachable[of xs S] by auto - obtain yt where yt_def: "yt : T & (dist yt xt < e)" - using e_def xst_def closure_approachable[of xt T] by auto - from ys_def yt_def have "dist (ys,yt) (xs,xt) < sqrt (2*e^2)" - unfolding dist_norm apply (auto simp add: norm_Pair) - using mult_strict_mono'[of "norm (ys - xs)" e "norm (ys - xs)" e] e_def - mult_strict_mono'[of "norm (yt - xt)" e "norm (yt - xt)" e] by (simp add: power2_eq_square) - hence "((ys,yt) : S <*> T) & (dist (ys,yt) x < 2*e)" - using e_def sqrt_add_le_add_sqrt[of "e^2" "e^2"] xst_def ys_def yt_def by auto - hence "EX y: S <*> T. dist y x < ee" using e_def by auto - } hence "x : closure (S <*> T)" using closure_approachable[of x "S <*> T"] by auto -} -hence "closure (S <*> T) >= closure S <*> closure T" by auto -moreover have "closed (closure S <*> closure T)" using closed_Times by auto -ultimately show ?thesis using closure_minimal[of "S <*> T" "closure S <*> closure T"] - closure_subset[of S] closure_subset[of T] by auto -qed + by (rule closure_Times) lemma closure_scaleR: (* TODO: generalize to real_normed_vector *) fixes S :: "('n::euclidean_space) set" diff -r 75ec83d45303 -r 5daa55003649 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Sun Aug 21 11:03:15 2011 -0700 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Sun Aug 21 12:22:31 2011 -0700 @@ -622,6 +622,23 @@ qed qed +lemma interior_Times: "interior (A \ B) = interior A \ interior B" +proof (rule interior_unique) + show "interior A \ interior B \ A \ B" + by (intro Sigma_mono interior_subset) + show "open (interior A \ interior B)" + by (intro open_Times open_interior) + show "\T. T \ A \ B \ open T \ T \ interior A \ interior B" + apply (simp add: open_prod_def, clarify) + apply (drule (1) bspec, clarify, rename_tac C D) + apply (simp add: interior_def, rule conjI) + apply (rule_tac x=C in exI, clarsimp) + apply (rule SigmaD1, erule subsetD, erule subsetD, erule (1) SigmaI) + apply (rule_tac x=D in exI, clarsimp) + apply (rule SigmaD2, erule subsetD, erule subsetD, erule (1) SigmaI) + done +qed + subsection {* Closure of a Set *} @@ -793,6 +810,23 @@ unfolding closure_interior by blast +lemma closure_Times: "closure (A \ B) = closure A \ closure B" +proof (intro closure_unique conjI) + show "A \ B \ closure A \ closure B" + by (intro Sigma_mono closure_subset) + show "closed (closure A \ closure B)" + by (intro closed_Times closed_closure) + show "\T. A \ B \ T \ closed T \ closure A \ closure B \ T" + apply (simp add: closed_def open_prod_def, clarify) + apply (rule ccontr) + apply (drule_tac x="(a, b)" in bspec, simp, clarify, rename_tac C D) + apply (simp add: closure_interior interior_def) + apply (drule_tac x=C in spec) + apply (drule_tac x=D in spec) + apply auto + done +qed + subsection {* Frontier (aka boundary) *}