equal
deleted
inserted
replaced
22 ("((_)/ ----> (_))" [60, 60] 60) where |
22 ("((_)/ ----> (_))" [60, 60] 60) where |
23 --{*Standard definition of convergence of sequence*} |
23 --{*Standard definition of convergence of sequence*} |
24 [code del]: "X ----> L = (\<forall>r>0. \<exists>no. \<forall>n\<ge>no. dist (X n) L < r)" |
24 [code del]: "X ----> L = (\<forall>r>0. \<exists>no. \<forall>n\<ge>no. dist (X n) L < r)" |
25 |
25 |
26 definition |
26 definition |
27 lim :: "(nat \<Rightarrow> 'a::real_normed_vector) \<Rightarrow> 'a" where |
27 lim :: "(nat \<Rightarrow> 'a::metric_space) \<Rightarrow> 'a" where |
28 --{*Standard definition of limit using choice operator*} |
28 --{*Standard definition of limit using choice operator*} |
29 "lim X = (THE L. X ----> L)" |
29 "lim X = (THE L. X ----> L)" |
30 |
30 |
31 definition |
31 definition |
32 convergent :: "(nat \<Rightarrow> 'a::metric_space) \<Rightarrow> bool" where |
32 convergent :: "(nat \<Rightarrow> 'a::metric_space) \<Rightarrow> bool" where |