--- 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"
--- 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 \<times> B) = interior A \<times> interior B"
+proof (rule interior_unique)
+ show "interior A \<times> interior B \<subseteq> A \<times> B"
+ by (intro Sigma_mono interior_subset)
+ show "open (interior A \<times> interior B)"
+ by (intro open_Times open_interior)
+ show "\<forall>T. T \<subseteq> A \<times> B \<and> open T \<longrightarrow> T \<subseteq> interior A \<times> 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 \<times> B) = closure A \<times> closure B"
+proof (intro closure_unique conjI)
+ show "A \<times> B \<subseteq> closure A \<times> closure B"
+ by (intro Sigma_mono closure_subset)
+ show "closed (closure A \<times> closure B)"
+ by (intro closed_Times closed_closure)
+ show "\<forall>T. A \<times> B \<subseteq> T \<and> closed T \<longrightarrow> closure A \<times> closure B \<subseteq> 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) *}