remove redundant lemma LIMSEQ_Complex in favor of tendsto_Complex
authorhuffman
Tue Sep 06 07:45:18 2011 -0700 (2011-09-06)
changeset 447487f6838b3474a
parent 44747 ab7522fbe1a2
child 44749 5b1e1432c320
remove redundant lemma LIMSEQ_Complex in favor of tendsto_Complex
NEWS
src/HOL/Complex.thy
     1.1 --- a/NEWS	Tue Sep 06 07:41:15 2011 -0700
     1.2 +++ b/NEWS	Tue Sep 06 07:45:18 2011 -0700
     1.3 @@ -301,6 +301,7 @@
     1.4    LIMSEQ_add_minus ~> tendsto_add [OF _ tendsto_minus]
     1.5    LIMSEQ_add_const ~> tendsto_add [OF _ tendsto_const]
     1.6    LIMSEQ_diff_const ~> tendsto_diff [OF _ tendsto_const]
     1.7 +  LIMSEQ_Complex ~> tendsto_Complex
     1.8    LIM_ident ~> tendsto_ident_at
     1.9    LIM_const ~> tendsto_const
    1.10    LIM_add ~> tendsto_add
     2.1 --- a/src/HOL/Complex.thy	Tue Sep 06 07:41:15 2011 -0700
     2.2 +++ b/src/HOL/Complex.thy	Tue Sep 06 07:45:18 2011 -0700
     2.3 @@ -366,10 +366,6 @@
     2.4         (simp add: dist_norm real_sqrt_sum_squares_less)
     2.5  qed
     2.6  
     2.7 -lemma LIMSEQ_Complex:
     2.8 -  "\<lbrakk>X ----> a; Y ----> b\<rbrakk> \<Longrightarrow> (\<lambda>n. Complex (X n) (Y n)) ----> Complex a b"
     2.9 -  by (rule tendsto_Complex)
    2.10 -
    2.11  instance complex :: banach
    2.12  proof
    2.13    fix X :: "nat \<Rightarrow> complex"
    2.14 @@ -379,7 +375,7 @@
    2.15    from Cauchy_Im [OF X] have 2: "(\<lambda>n. Im (X n)) ----> lim (\<lambda>n. Im (X n))"
    2.16      by (simp add: Cauchy_convergent_iff convergent_LIMSEQ_iff)
    2.17    have "X ----> Complex (lim (\<lambda>n. Re (X n))) (lim (\<lambda>n. Im (X n)))"
    2.18 -    using LIMSEQ_Complex [OF 1 2] by simp
    2.19 +    using tendsto_Complex [OF 1 2] by simp
    2.20    thus "convergent X"
    2.21      by (rule convergentI)
    2.22  qed