author huffman Thu, 11 Jun 2009 12:05:41 -0700 changeset 31566 eff95000aae7 parent 31565 da5a5589418e child 31567 0fb78b3a9145
new lemmas
```--- 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"```