src/HOL/Hyperreal/HyperNat.thy
changeset 20695 1cc6fefbff1a
parent 20552 2c31dd358c21
child 20730 da903f59e9ba
--- a/src/HOL/Hyperreal/HyperNat.thy	Sun Sep 24 07:14:02 2006 +0200
+++ b/src/HOL/Hyperreal/HyperNat.thy	Sun Sep 24 07:18:16 2006 +0200
@@ -157,6 +157,16 @@
 follows because member @{term FreeUltrafilterNat} is not finite.
 See @{text HyperDef.thy} for similar argument.*}
 
+text{* Example of an hypersequence (i.e. an extended standard sequence)
+   whose term with an hypernatural suffix is an infinitesimal i.e.
+   the whn'nth term of the hypersequence is a member of Infinitesimal*}
+
+lemma SEQ_Infinitesimal:
+      "( *f* (%n::nat. inverse(real(Suc n)))) whn : Infinitesimal"
+apply (simp add: hypnat_omega_def starfun star_n_inverse)
+apply (simp add: Infinitesimal_FreeUltrafilterNat_iff)
+apply (simp add: real_of_nat_Suc_gt_zero FreeUltrafilterNat_inverse_real_of_posnat)
+done
 
 lemma lemma_unbounded_set [simp]: "{n::nat. m < n} \<in> FreeUltrafilterNat"
 apply (insert finite_atMost [of m])