src/HOL/Complex.thy
changeset 44748 7f6838b3474a
parent 44724 0b900a9d8023
child 44749 5b1e1432c320
     1.1 --- a/src/HOL/Complex.thy	Tue Sep 06 07:41:15 2011 -0700
     1.2 +++ b/src/HOL/Complex.thy	Tue Sep 06 07:45:18 2011 -0700
     1.3 @@ -366,10 +366,6 @@
     1.4         (simp add: dist_norm real_sqrt_sum_squares_less)
     1.5  qed
     1.6  
     1.7 -lemma LIMSEQ_Complex:
     1.8 -  "\<lbrakk>X ----> a; Y ----> b\<rbrakk> \<Longrightarrow> (\<lambda>n. Complex (X n) (Y n)) ----> Complex a b"
     1.9 -  by (rule tendsto_Complex)
    1.10 -
    1.11  instance complex :: banach
    1.12  proof
    1.13    fix X :: "nat \<Rightarrow> complex"
    1.14 @@ -379,7 +375,7 @@
    1.15    from Cauchy_Im [OF X] have 2: "(\<lambda>n. Im (X n)) ----> lim (\<lambda>n. Im (X n))"
    1.16      by (simp add: Cauchy_convergent_iff convergent_LIMSEQ_iff)
    1.17    have "X ----> Complex (lim (\<lambda>n. Re (X n))) (lim (\<lambda>n. Im (X n)))"
    1.18 -    using LIMSEQ_Complex [OF 1 2] by simp
    1.19 +    using tendsto_Complex [OF 1 2] by simp
    1.20    thus "convergent X"
    1.21      by (rule convergentI)
    1.22  qed