src/HOL/Hyperreal/SEQ.thy
changeset 15085 5693a977a767
parent 15082 6c3276a2735b
child 15102 04b0e943fcc9
equal deleted inserted replaced
15084:07f7b158ef32 15085:5693a977a767
   794 apply (drule lemma_trans4)
   794 apply (drule lemma_trans4)
   795 apply (drule_tac [2] lemma_trans4)
   795 apply (drule_tac [2] lemma_trans4)
   796 apply (rule_tac x = "1 + \<bar>X M\<bar> " in exI)
   796 apply (rule_tac x = "1 + \<bar>X M\<bar> " in exI)
   797 apply (rule_tac [2] x = "1 + \<bar>X M\<bar> " in exI)
   797 apply (rule_tac [2] x = "1 + \<bar>X M\<bar> " in exI)
   798 apply (rule_tac [3] x = "\<bar>X m\<bar> " in exI)
   798 apply (rule_tac [3] x = "\<bar>X m\<bar> " in exI)
   799 apply (auto elim!: lemma_Nat_covered, arith+)
   799 apply (auto elim!: lemma_Nat_covered)
   800 done
   800 done
   801 
   801 
   802 text{*A Cauchy sequence is bounded -- nonstandard version*}
   802 text{*A Cauchy sequence is bounded -- nonstandard version*}
   803 
   803 
   804 lemma NSCauchy_NSBseq: "NSCauchy X ==> NSBseq X"
   804 lemma NSCauchy_NSBseq: "NSCauchy X ==> NSBseq X"