# HG changeset patch
# User huffman
# Date 1244762766 25200
# Node ID 963caf6fa23491077ac433e3f2fd3b1693ab586c
# Parent  0fb78b3a914532011f879804ac4069bbaafe6c27
add lemmas about closed sets

diff -r 0fb78b3a9145 -r 963caf6fa234 src/HOL/Library/Euclidean_Space.thy
--- 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"
diff -r 0fb78b3a9145 -r 963caf6fa234 src/HOL/Library/Product_Vector.thy
--- 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