equal
deleted
inserted
replaced
119 qed |
119 qed |
120 |
120 |
121 subsection {* Cauchy sequences *} |
121 subsection {* Cauchy sequences *} |
122 |
122 |
123 definition |
123 definition |
124 cauchy :: "(nat \<Rightarrow> rat) set" |
124 cauchy :: "(nat \<Rightarrow> rat) \<Rightarrow> bool" |
125 where |
125 where |
126 "cauchy X \<longleftrightarrow> (\<forall>r>0. \<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. \<bar>X m - X n\<bar> < r)" |
126 "cauchy X \<longleftrightarrow> (\<forall>r>0. \<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. \<bar>X m - X n\<bar> < r)" |
127 |
127 |
128 lemma cauchyI: |
128 lemma cauchyI: |
129 "(\<And>r. 0 < r \<Longrightarrow> \<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. \<bar>X m - X n\<bar> < r) \<Longrightarrow> cauchy X" |
129 "(\<And>r. 0 < r \<Longrightarrow> \<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. \<bar>X m - X n\<bar> < r) \<Longrightarrow> cauchy X" |