equal
deleted
inserted
replaced
9 imports NSComplex |
9 imports NSComplex |
10 begin |
10 begin |
11 |
11 |
12 definition |
12 definition |
13 (* standard complex numbers reagarded as an embedded subset of NS complex *) |
13 (* standard complex numbers reagarded as an embedded subset of NS complex *) |
14 SComplex :: "hcomplex set" |
14 SComplex :: "hcomplex set" where |
15 "SComplex = {x. \<exists>r. x = hcomplex_of_complex r}" |
15 "SComplex = {x. \<exists>r. x = hcomplex_of_complex r}" |
16 |
16 |
17 stc :: "hcomplex => hcomplex" |
17 definition |
|
18 stc :: "hcomplex => hcomplex" where |
18 --{* standard part map*} |
19 --{* standard part map*} |
19 "stc x = (SOME r. x \<in> HFinite & r:SComplex & r @= x)" |
20 "stc x = (SOME r. x \<in> HFinite & r:SComplex & r @= x)" |
20 |
21 |
21 |
22 |
22 subsection{*Closure Laws for SComplex, the Standard Complex Numbers*} |
23 subsection{*Closure Laws for SComplex, the Standard Complex Numbers*} |