src/HOL/RealDef.thy
changeset 44278 1220ecb81e8f
parent 43887 442aceb54969
child 44344 49be3e7d4762
equal deleted inserted replaced
44277:bcb696533579 44278:1220ecb81e8f
   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"