equal
deleted
inserted
replaced
155 |
155 |
156 text{*Existence of infinite number not corresponding to any natural number |
156 text{*Existence of infinite number not corresponding to any natural number |
157 follows because member @{term FreeUltrafilterNat} is not finite. |
157 follows because member @{term FreeUltrafilterNat} is not finite. |
158 See @{text HyperDef.thy} for similar argument.*} |
158 See @{text HyperDef.thy} for similar argument.*} |
159 |
159 |
|
160 text{* Example of an hypersequence (i.e. an extended standard sequence) |
|
161 whose term with an hypernatural suffix is an infinitesimal i.e. |
|
162 the whn'nth term of the hypersequence is a member of Infinitesimal*} |
|
163 |
|
164 lemma SEQ_Infinitesimal: |
|
165 "( *f* (%n::nat. inverse(real(Suc n)))) whn : Infinitesimal" |
|
166 apply (simp add: hypnat_omega_def starfun star_n_inverse) |
|
167 apply (simp add: Infinitesimal_FreeUltrafilterNat_iff) |
|
168 apply (simp add: real_of_nat_Suc_gt_zero FreeUltrafilterNat_inverse_real_of_posnat) |
|
169 done |
160 |
170 |
161 lemma lemma_unbounded_set [simp]: "{n::nat. m < n} \<in> FreeUltrafilterNat" |
171 lemma lemma_unbounded_set [simp]: "{n::nat. m < n} \<in> FreeUltrafilterNat" |
162 apply (insert finite_atMost [of m]) |
172 apply (insert finite_atMost [of m]) |
163 apply (simp add: atMost_def) |
173 apply (simp add: atMost_def) |
164 apply (drule FreeUltrafilterNat_finite) |
174 apply (drule FreeUltrafilterNat_finite) |