454 (*------------------------------------------------------------------- |
454 (*------------------------------------------------------------------- |
455 Another characterization of Infinitesimal and one of @= relation. |
455 Another characterization of Infinitesimal and one of @= relation. |
456 In this theory since hypreal_hrabs proved here. (To Check:) Maybe |
456 In this theory since hypreal_hrabs proved here. (To Check:) Maybe |
457 move both if possible? |
457 move both if possible? |
458 -------------------------------------------------------------------*) |
458 -------------------------------------------------------------------*) |
459 lemma Infinitesimal_FreeUltrafilterNat_iff2: "(x:Infinitesimal) = |
459 lemma Infinitesimal_FreeUltrafilterNat_iff2: |
|
460 "(x:Infinitesimal) = |
460 (EX X:Rep_hypreal(x). |
461 (EX X:Rep_hypreal(x). |
461 ALL m. {n. abs(X n) < inverse(real(Suc m))} |
462 ALL m. {n. abs(X n) < inverse(real(Suc m))} |
462 : FreeUltrafilterNat)" |
463 : FreeUltrafilterNat)" |
463 apply (rule_tac z = x in eq_Abs_hypreal) |
464 apply (rule eq_Abs_hypreal [of x]) |
464 apply (auto intro!: bexI lemma_hyprel_refl |
465 apply (auto intro!: bexI lemma_hyprel_refl |
465 simp add: Infinitesimal_hypreal_of_nat_iff hypreal_of_real_def |
466 simp add: Infinitesimal_hypreal_of_nat_iff hypreal_of_real_def |
466 hypreal_inverse hypreal_hrabs hypreal_less hypreal_of_nat_def) |
467 hypreal_inverse hypreal_hrabs hypreal_less hypreal_of_nat_eq) |
467 apply (drule_tac x = n in spec, ultra) |
468 apply (drule_tac x = n in spec, ultra) |
468 done |
469 done |
469 |
470 |
470 lemma approx_FreeUltrafilterNat_iff: "(Abs_hypreal(hyprel``{X}) @= Abs_hypreal(hyprel``{Y})) = |
471 lemma approx_FreeUltrafilterNat_iff: "(Abs_hypreal(hyprel``{X}) @= Abs_hypreal(hyprel``{Y})) = |
471 (ALL m. {n. abs (X n + - Y n) < |
472 (ALL m. {n. abs (X n + - Y n) < |