1.1 --- a/src/HOL/Library/Euclidean_Space.thy Thu Jun 11 15:33:13 2009 -0700
1.2 +++ b/src/HOL/Library/Euclidean_Space.thy Thu Jun 11 16:26:06 2009 -0700
1.3 @@ -378,6 +378,17 @@
1.4 apply (rule_tac x="\<lambda>k. if k = i then S else UNIV" in exI, simp)
1.5 done
1.6
1.7 +lemma closed_vimage_Cart_nth: "closed S \<Longrightarrow> closed ((\<lambda>x. x $ i) -` S)"
1.8 +unfolding closed_open vimage_Compl [symmetric]
1.9 +by (rule open_vimage_Cart_nth)
1.10 +
1.11 +lemma closed_vector_box: "\<forall>i. closed (S i) \<Longrightarrow> closed {x. \<forall>i. x $ i \<in> S i}"
1.12 +proof -
1.13 + have "{x. \<forall>i. x $ i \<in> S i} = (\<Inter>i. (\<lambda>x. x $ i) -` S i)" by auto
1.14 + thus "\<forall>i. closed (S i) \<Longrightarrow> closed {x. \<forall>i. x $ i \<in> S i}"
1.15 + by (simp add: closed_INT closed_vimage_Cart_nth)
1.16 +qed
1.17 +
1.18 lemma tendsto_Cart_nth [tendsto_intros]:
1.19 assumes "((\<lambda>x. f x) ---> a) net"
1.20 shows "((\<lambda>x. f x $ i) ---> a $ i) net"

2.1 --- a/src/HOL/Library/Product_Vector.thy Thu Jun 11 15:33:13 2009 -0700
2.2 +++ b/src/HOL/Library/Product_Vector.thy Thu Jun 11 16:26:06 2009 -0700
2.3 @@ -87,6 +87,22 @@
2.4 lemma open_vimage_snd: "open S \<Longrightarrow> open (snd -` S)"
2.5 by (simp add: snd_vimage_eq_Times open_Times)
2.6
2.7 +lemma closed_vimage_fst: "closed S \<Longrightarrow> closed (fst -` S)"
2.8 +unfolding closed_open vimage_Compl [symmetric]
2.9 +by (rule open_vimage_fst)
2.10 +
2.11 +lemma closed_vimage_snd: "closed S \<Longrightarrow> closed (snd -` S)"
2.12 +unfolding closed_open vimage_Compl [symmetric]
2.13 +by (rule open_vimage_snd)
2.14 +
2.15 +lemma closed_Times: "closed S \<Longrightarrow> closed T \<Longrightarrow> closed (S \<times> T)"
2.16 +proof -
2.17 + have "S \<times> T = (fst -` S) \<inter> (snd -` T)" by auto
2.18 + thus "closed S \<Longrightarrow> closed T \<Longrightarrow> closed (S \<times> T)"
2.19 + by (simp add: closed_vimage_fst closed_vimage_snd closed_Int)
2.20 +qed
2.21 +
2.22 +
2.23 subsection {* Product is a metric space *}
2.24
2.25 instantiation