src/HOL/Library/Fundamental_Theorem_Algebra.thy
changeset 31337 a9ed5fcc5e39
parent 31021 53642251a04f
child 32456 341c83339aeb
     1.1 --- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Thu May 28 22:57:17 2009 -0700
     1.2 +++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Thu May 28 23:03:12 2009 -0700
     1.3 @@ -306,12 +306,12 @@
     1.4    from conv1[unfolded convergent_def] obtain x where "LIMSEQ (\<lambda>n. Re (s (f n))) x"
     1.5      by blast
     1.6    hence  x: "\<forall>r>0. \<exists>n0. \<forall>n\<ge>n0. \<bar> Re (s (f n)) - x \<bar> < r"
     1.7 -    unfolding LIMSEQ_def real_norm_def .
     1.8 +    unfolding LIMSEQ_iff real_norm_def .
     1.9  
    1.10    from conv2[unfolded convergent_def] obtain y where "LIMSEQ (\<lambda>n. Im (s (f (g n)))) y"
    1.11      by blast
    1.12    hence  y: "\<forall>r>0. \<exists>n0. \<forall>n\<ge>n0. \<bar> Im (s (f (g n))) - y \<bar> < r"
    1.13 -    unfolding LIMSEQ_def real_norm_def .
    1.14 +    unfolding LIMSEQ_iff real_norm_def .
    1.15    let ?w = "Complex x y"
    1.16    from f(1) g(1) have hs: "subseq ?h" unfolding subseq_def by auto
    1.17    {fix e assume ep: "e > (0::real)"