# HG changeset patch
# User huffman
# Date 1244747141 25200
# Node ID eff95000aae74d0b9ad2abf6ff4ebd458508cf59
# Parent  da5a5589418e176505f70f90c958e9a2326eb80b
new lemmas

diff -r da5a5589418e -r eff95000aae7 src/HOL/Library/Euclidean_Space.thy
--- a/src/HOL/Library/Euclidean_Space.thy	Thu Jun 11 11:51:12 2009 -0700
+++ b/src/HOL/Library/Euclidean_Space.thy	Thu Jun 11 12:05:41 2009 -0700
@@ -369,19 +369,22 @@
 
 end
 
-lemma tendsto_Cart_nth:
-  fixes f :: "'a \<Rightarrow> 'b::topological_space ^ 'n::finite"
+lemma open_vector_box: "\<forall>i. open (S i) \<Longrightarrow> open {x. \<forall>i. x $ i \<in> S i}"
+unfolding open_vector_def by auto
+
+lemma open_vimage_Cart_nth: "open S \<Longrightarrow> open ((\<lambda>x. x $ i) -` S)"
+unfolding open_vector_def
+apply clarify
+apply (rule_tac x="\<lambda>k. if k = i then S else UNIV" in exI, simp)
+done
+
+lemma tendsto_Cart_nth [tendsto_intros]:
   assumes "((\<lambda>x. f x) ---> a) net"
   shows "((\<lambda>x. f x $ i) ---> a $ i) net"
 proof (rule topological_tendstoI)
-  fix S :: "'b set" assume "open S" "a $ i \<in> S"
+  fix S assume "open S" "a $ i \<in> S"
   then have "open ((\<lambda>y. y $ i) -` S)" "a \<in> ((\<lambda>y. y $ i) -` S)"
-    unfolding open_vector_def
-    apply simp_all
-    apply clarify
-    apply (rule_tac x="\<lambda>k. if k = i then S else UNIV" in exI)
-    apply simp
-    done
+    by (simp_all add: open_vimage_Cart_nth)
   with assms have "eventually (\<lambda>x. f x \<in> (\<lambda>y. y $ i) -` S) net"
     by (rule topological_tendstoD)
   then show "eventually (\<lambda>x. f x $ i \<in> S) net"