327 by (simp add: Infinitesimal_hypreal_of_nat_iff star_of_def |
327 by (simp add: Infinitesimal_hypreal_of_nat_iff star_of_def |
328 hnorm_def star_of_nat_def starfun_star_n |
328 hnorm_def star_of_nat_def starfun_star_n |
329 star_n_inverse star_n_less hypreal_of_nat_eq) |
329 star_n_inverse star_n_less hypreal_of_nat_eq) |
330 |
330 |
331 lemma approx_FreeUltrafilterNat_iff: "star_n X @= star_n Y = |
331 lemma approx_FreeUltrafilterNat_iff: "star_n X @= star_n Y = |
332 (\<forall>r>0. {n. norm (X n + - Y n) < r} : FreeUltrafilterNat)" |
332 (\<forall>r>0. {n. norm (X n - Y n) < r} : FreeUltrafilterNat)" |
333 apply (subst approx_minus_iff) |
333 apply (subst approx_minus_iff) |
334 apply (rule mem_infmal_iff [THEN subst]) |
334 apply (rule mem_infmal_iff [THEN subst]) |
335 apply (simp add: star_n_minus star_n_add) |
335 apply (simp add: star_n_diff) |
336 apply (simp add: Infinitesimal_FreeUltrafilterNat_iff) |
336 apply (simp add: Infinitesimal_FreeUltrafilterNat_iff) |
337 done |
337 done |
338 |
338 |
339 lemma approx_FreeUltrafilterNat_iff2: "star_n X @= star_n Y = |
339 lemma approx_FreeUltrafilterNat_iff2: "star_n X @= star_n Y = |
340 (\<forall>m. {n. norm (X n + - Y n) < |
340 (\<forall>m. {n. norm (X n - Y n) < |
341 inverse(real(Suc m))} : FreeUltrafilterNat)" |
341 inverse(real(Suc m))} : FreeUltrafilterNat)" |
342 apply (subst approx_minus_iff) |
342 apply (subst approx_minus_iff) |
343 apply (rule mem_infmal_iff [THEN subst]) |
343 apply (rule mem_infmal_iff [THEN subst]) |
344 apply (simp add: star_n_minus star_n_add) |
344 apply (simp add: star_n_diff) |
345 apply (simp add: Infinitesimal_FreeUltrafilterNat_iff2) |
345 apply (simp add: Infinitesimal_FreeUltrafilterNat_iff2) |
346 done |
346 done |
347 |
347 |
348 lemma inj_starfun: "inj starfun" |
348 lemma inj_starfun: "inj starfun" |
349 apply (rule inj_onI) |
349 apply (rule inj_onI) |