--- a/src/HOL/Library/Product_Vector.thy Tue May 04 09:56:34 2010 -0700
+++ b/src/HOL/Library/Product_Vector.thy Tue May 04 10:06:05 2010 -0700
@@ -312,18 +312,6 @@
(simp add: subsetD [OF `A \<times> B \<subseteq> S`])
qed
-lemma LIMSEQ_fst: "(X ----> a) \<Longrightarrow> (\<lambda>n. fst (X n)) ----> fst a"
-unfolding LIMSEQ_conv_tendsto by (rule tendsto_fst)
-
-lemma LIMSEQ_snd: "(X ----> a) \<Longrightarrow> (\<lambda>n. snd (X n)) ----> snd a"
-unfolding LIMSEQ_conv_tendsto by (rule tendsto_snd)
-
-lemma LIMSEQ_Pair:
- assumes "X ----> a" and "Y ----> b"
- shows "(\<lambda>n. (X n, Y n)) ----> (a, b)"
-using assms unfolding LIMSEQ_conv_tendsto
-by (rule tendsto_Pair)
-
lemma LIM_fst: "f -- x --> a \<Longrightarrow> (\<lambda>x. fst (f x)) -- x --> fst a"
unfolding LIM_conv_tendsto by (rule tendsto_fst)
@@ -374,7 +362,7 @@
using Cauchy_snd [OF `Cauchy X`]
by (simp add: Cauchy_convergent_iff convergent_LIMSEQ_iff)
have "X ----> (lim (\<lambda>n. fst (X n)), lim (\<lambda>n. snd (X n)))"
- using LIMSEQ_Pair [OF 1 2] by simp
+ using tendsto_Pair [OF 1 2] by simp
then show "convergent X"
by (rule convergentI)
qed