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