equal
deleted
inserted
replaced
68 the whn'nth term of the hypersequence is a member of Infinitesimal*} |
68 the whn'nth term of the hypersequence is a member of Infinitesimal*} |
69 |
69 |
70 lemma SEQ_Infinitesimal: |
70 lemma SEQ_Infinitesimal: |
71 "( *f* (%n::nat. inverse(real(Suc n)))) whn : Infinitesimal" |
71 "( *f* (%n::nat. inverse(real(Suc n)))) whn : Infinitesimal" |
72 apply (simp add: hypnat_omega_def Infinitesimal_FreeUltrafilterNat_iff starfun) |
72 apply (simp add: hypnat_omega_def Infinitesimal_FreeUltrafilterNat_iff starfun) |
73 apply (simp add: star_n_inverse2) |
73 apply (simp add: star_n_inverse) |
74 apply (rule bexI [OF _ Rep_star_star_n]) |
74 apply (rule bexI [OF _ Rep_star_star_n]) |
75 apply (simp add: real_of_nat_Suc_gt_zero FreeUltrafilterNat_inverse_real_of_posnat) |
75 apply (simp add: real_of_nat_Suc_gt_zero FreeUltrafilterNat_inverse_real_of_posnat) |
76 done |
76 done |
77 |
77 |
78 |
78 |