src/HOL/SEQ.thy
changeset 44205 18da2a87421c
parent 44194 0639898074ae
child 44206 5e4a1664106e
     1.1 --- a/src/HOL/SEQ.thy	Sun Aug 14 08:45:38 2011 -0700
     1.2 +++ b/src/HOL/SEQ.thy	Sun Aug 14 10:25:43 2011 -0700
     1.3 @@ -189,7 +189,7 @@
     1.4    "X ----> L \<equiv> (X ---> L) sequentially"
     1.5  
     1.6  definition
     1.7 -  lim :: "(nat \<Rightarrow> 'a::metric_space) \<Rightarrow> 'a" where
     1.8 +  lim :: "(nat \<Rightarrow> 'a::t2_space) \<Rightarrow> 'a" where
     1.9      --{*Standard definition of limit using choice operator*}
    1.10    "lim X = (THE L. X ----> L)"
    1.11  
    1.12 @@ -301,9 +301,9 @@
    1.13  by (rule tendsto_const)
    1.14  
    1.15  lemma LIMSEQ_const_iff:
    1.16 -  fixes k l :: "'a::metric_space"
    1.17 +  fixes k l :: "'a::t2_space"
    1.18    shows "(\<lambda>n. k) ----> l \<longleftrightarrow> k = l"
    1.19 -by (rule tendsto_const_iff, rule sequentially_bot)
    1.20 +  using trivial_limit_sequentially by (rule tendsto_const_iff)
    1.21  
    1.22  lemma LIMSEQ_norm:
    1.23    fixes a :: "'a::real_normed_vector"
    1.24 @@ -366,9 +366,9 @@
    1.25  by (rule tendsto_diff)
    1.26  
    1.27  lemma LIMSEQ_unique:
    1.28 -  fixes a b :: "'a::metric_space"
    1.29 +  fixes a b :: "'a::t2_space"
    1.30    shows "\<lbrakk>X ----> a; X ----> b\<rbrakk> \<Longrightarrow> a = b"
    1.31 -by (drule (1) tendsto_dist, simp add: LIMSEQ_const_iff)
    1.32 +  using trivial_limit_sequentially by (rule tendsto_unique)
    1.33  
    1.34  lemma (in bounded_linear) LIMSEQ:
    1.35    "X ----> a \<Longrightarrow> (\<lambda>n. f (X n)) ----> f a"