Mercurial > hg > Members > kono > Proof > HyperReal

changeset 21:5e4b38745a39

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 09 Jul 2021 08:08:39 +0900
parents a839f149825f
children 942f4e528a79
files src/HyperReal.agda
diffstat 1 files changed, 16 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
--- a/src/HyperReal.agda	Thu Jul 08 17:14:30 2021 +0900
+++ b/src/HyperReal.agda	Fri Jul 09 08:08:39 2021 +0900
@@ -248,11 +248,23 @@
 _≈_ : (x y : HyperR ) → Set
 x ≈ y = inifinitesimal-R (x h+ ( -h y )) 
 
-record Real : Set
+is-inifinitesimal : {x : HyperR } → inifinitesimal-R x → x ≈ R0
+is-inifinitesimal {x} inf = {!!}
+
+record Standard : Set where
    field
-      st          : HyperR → HyperR
-      is-st       : (x : HyperR ) → x ≈ st x
-      st-unique   : (x y : HyperR ) → st x ≡ st y
+      standard          : HyperR → HyperR
+      is-standard       : {x : HyperR } → x ≈ standard x
+      standard-unique   : {x y : HyperR } →  x ≈ y → standard x ≡ standard y
+      st-inifinitesimal : {x : HyperR } → inifinitesimal-R x → st x ≡ R0
+
+postulate
+   ST : Standard
+
+open Standard
+
+st :  HyperR → HyperR
+st x = standard ST x