author huffman Thu, 11 Jun 2009 16:26:06 -0700 changeset 31568 963caf6fa234 parent 31567 0fb78b3a9145 child 31569 f11a849bab61
```--- 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)"

+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```