src/HOL/Complex.thy
changeset 61969 e01015e49041
parent 61944 5d06ecfdb472
child 61973 0c7e865fa7cb
     1.1 --- a/src/HOL/Complex.thy	Tue Dec 29 22:41:22 2015 +0100
     1.2 +++ b/src/HOL/Complex.thy	Tue Dec 29 23:04:53 2015 +0100
     1.3 @@ -415,7 +415,7 @@
     1.4  proof
     1.5    fix X :: "nat \<Rightarrow> complex"
     1.6    assume X: "Cauchy X"
     1.7 -  then have "(\<lambda>n. Complex (Re (X n)) (Im (X n))) ----> Complex (lim (\<lambda>n. Re (X n))) (lim (\<lambda>n. Im (X n)))"
     1.8 +  then have "(\<lambda>n. Complex (Re (X n)) (Im (X n))) \<longlonglongrightarrow> Complex (lim (\<lambda>n. Re (X n))) (lim (\<lambda>n. Im (X n)))"
     1.9      by (intro tendsto_Complex convergent_LIMSEQ_iff[THEN iffD1] Cauchy_convergent_iff[THEN iffD1] Cauchy_Re Cauchy_Im)
    1.10    then show "convergent X"
    1.11      unfolding complex.collapse by (rule convergentI)