--- a/src/HOL/Library/Euclidean_Space.thy Thu Jun 11 15:33:13 2009 -0700
+++ b/src/HOL/Library/Euclidean_Space.thy Thu Jun 11 16:26:06 2009 -0700
@@ -378,6 +378,17 @@
apply (rule_tac x="\<lambda>k. if k = i then S else UNIV" in exI, simp)
done
+lemma closed_vimage_Cart_nth: "closed S \<Longrightarrow> closed ((\<lambda>x. x $ i) -` S)"
+unfolding closed_open vimage_Compl [symmetric]
+by (rule open_vimage_Cart_nth)
+
+lemma closed_vector_box: "\<forall>i. closed (S i) \<Longrightarrow> closed {x. \<forall>i. x $ i \<in> S i}"
+proof -
+ have "{x. \<forall>i. x $ i \<in> S i} = (\<Inter>i. (\<lambda>x. x $ i) -` S i)" by auto
+ thus "\<forall>i. closed (S i) \<Longrightarrow> closed {x. \<forall>i. x $ i \<in> S i}"
+ by (simp add: closed_INT closed_vimage_Cart_nth)
+qed
+
lemma tendsto_Cart_nth [tendsto_intros]:
assumes "((\<lambda>x. f x) ---> a) net"
shows "((\<lambda>x. f x $ i) ---> a $ i) net"
--- a/src/HOL/Library/Product_Vector.thy Thu Jun 11 15:33:13 2009 -0700
+++ b/src/HOL/Library/Product_Vector.thy Thu Jun 11 16:26:06 2009 -0700
@@ -87,6 +87,22 @@
lemma open_vimage_snd: "open S \<Longrightarrow> open (snd -` S)"
by (simp add: snd_vimage_eq_Times open_Times)
+lemma closed_vimage_fst: "closed S \<Longrightarrow> closed (fst -` S)"
+unfolding closed_open vimage_Compl [symmetric]
+by (rule open_vimage_fst)
+
+lemma closed_vimage_snd: "closed S \<Longrightarrow> closed (snd -` S)"
+unfolding closed_open vimage_Compl [symmetric]
+by (rule open_vimage_snd)
+
+lemma closed_Times: "closed S \<Longrightarrow> closed T \<Longrightarrow> closed (S \<times> T)"
+proof -
+ have "S \<times> T = (fst -` S) \<inter> (snd -` T)" by auto
+ thus "closed S \<Longrightarrow> closed T \<Longrightarrow> closed (S \<times> T)"
+ by (simp add: closed_vimage_fst closed_vimage_snd closed_Int)
+qed
+
+
subsection {* Product is a metric space *}
instantiation