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"
```