# HG changeset patch
# User huffman
# Date 1315320318 25200
# Node ID 7f6838b3474a45638fedab1dd6c1bbc3a6ccdcd0
# Parent  ab7522fbe1a254a4596aa9898662cb34e87f4305
remove redundant lemma LIMSEQ_Complex in favor of tendsto_Complex

diff -r ab7522fbe1a2 -r 7f6838b3474a NEWS
--- a/NEWS	Tue Sep 06 07:41:15 2011 -0700
+++ b/NEWS	Tue Sep 06 07:45:18 2011 -0700
@@ -301,6 +301,7 @@
   LIMSEQ_add_minus ~> tendsto_add [OF _ tendsto_minus]
   LIMSEQ_add_const ~> tendsto_add [OF _ tendsto_const]
   LIMSEQ_diff_const ~> tendsto_diff [OF _ tendsto_const]
+  LIMSEQ_Complex ~> tendsto_Complex
   LIM_ident ~> tendsto_ident_at
   LIM_const ~> tendsto_const
   LIM_add ~> tendsto_add
diff -r ab7522fbe1a2 -r 7f6838b3474a src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Tue Sep 06 07:41:15 2011 -0700
+++ b/src/HOL/Complex.thy	Tue Sep 06 07:45:18 2011 -0700
@@ -366,10 +366,6 @@
        (simp add: dist_norm real_sqrt_sum_squares_less)
 qed
 
-lemma LIMSEQ_Complex:
-  "\<lbrakk>X ----> a; Y ----> b\<rbrakk> \<Longrightarrow> (\<lambda>n. Complex (X n) (Y n)) ----> Complex a b"
-  by (rule tendsto_Complex)
-
 instance complex :: banach
 proof
   fix X :: "nat \<Rightarrow> complex"
@@ -379,7 +375,7 @@
   from Cauchy_Im [OF X] have 2: "(\<lambda>n. Im (X n)) ----> lim (\<lambda>n. Im (X n))"
     by (simp add: Cauchy_convergent_iff convergent_LIMSEQ_iff)
   have "X ----> Complex (lim (\<lambda>n. Re (X n))) (lim (\<lambda>n. Im (X n)))"
-    using LIMSEQ_Complex [OF 1 2] by simp
+    using tendsto_Complex [OF 1 2] by simp
   thus "convergent X"
     by (rule convergentI)
 qed