src/HOL/SEQ.thy
 changeset 44206 5e4a1664106e parent 44205 18da2a87421c child 44208 1d2bf1f240ac
```     1.1 --- a/src/HOL/SEQ.thy	Sun Aug 14 10:25:43 2011 -0700
1.2 +++ b/src/HOL/SEQ.thy	Sun Aug 14 10:47:47 2011 -0700
1.3 @@ -183,8 +183,8 @@
1.4
1.5  subsection {* Defintions of limits *}
1.6
1.7 -abbreviation
1.8 -  LIMSEQ :: "[nat \<Rightarrow> 'a::topological_space, 'a] \<Rightarrow> bool"
1.9 +abbreviation (in topological_space)
1.10 +  LIMSEQ :: "[nat \<Rightarrow> 'a, 'a] \<Rightarrow> bool"
1.11      ("((_)/ ----> (_))" [60, 60] 60) where
1.12    "X ----> L \<equiv> (X ---> L) sequentially"
1.13
1.14 @@ -193,9 +193,7 @@
1.15      --{*Standard definition of limit using choice operator*}
1.16    "lim X = (THE L. X ----> L)"
1.17
1.18 -definition
1.19 -  convergent :: "(nat \<Rightarrow> 'a::metric_space) \<Rightarrow> bool" where
1.20 -    --{*Standard definition of convergence*}
1.21 +definition (in topological_space) convergent :: "(nat \<Rightarrow> 'a) \<Rightarrow> bool" where
1.22    "convergent X = (\<exists>L. X ----> L)"
1.23
1.24  definition
1.25 @@ -203,9 +201,7 @@
1.26      --{*Standard definition for bounded sequence*}
1.27    "Bseq X = (\<exists>K>0.\<forall>n. norm (X n) \<le> K)"
1.28
1.29 -definition
1.30 -  Cauchy :: "(nat \<Rightarrow> 'a::metric_space) \<Rightarrow> bool" where
1.31 -    --{*Standard definition of the Cauchy condition*}
1.32 +definition (in metric_space) Cauchy :: "(nat \<Rightarrow> 'a) \<Rightarrow> bool" where
1.33    "Cauchy X = (\<forall>e>0. \<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. dist (X m) (X n) < e)"
1.34
1.35
1.36 @@ -977,7 +973,7 @@
1.37
1.38  subsubsection {* Cauchy Sequences are Convergent *}
1.39
1.40 -class complete_space =
1.41 +class complete_space = metric_space +
1.42    assumes Cauchy_convergent: "Cauchy X \<Longrightarrow> convergent X"
1.43
1.44  class banach = real_normed_vector + complete_space
```