setname1
http://www.openmath.org/cd/setname1.ocd
2003-04-01
2001-03-12
2
0
official
alg1
arith1
logic1
quant1
relation1
set1
nums1
This CD defines common sets of mathematics
Written by J.H. Davenport on 1999-04-18.
Revised to add Zm, GFp, GFpn on 1999-11-09.
Revised to add QuotientField and A on 1999-11-19.
P
This symbol represents the set of positive prime numbers.
for all n |
n is a positive prime number is equivalent to:
n is a natural number and n > 1 and
((n=a*b and a and b are natural numbers) implies ((a=1 and b=n) or
(b=1 and a=n)))
N
This symbol represents the set of natural numbers (including zero).
for all n | n in the natural numbers is equivalent to saying
n=0 or n-1 is a natural number
Z
This symbol represents the set of integers, positive, negative and zero.
for all z | the statements z is an integer and z is a natural number
or -z is a natural number are equivalent
Q
This symbol represents the set of rational numbers.
for all z where z is a rational, there exists integers p and q with
q > 1 and p/q = z
for all a,b | a,b rational with a<b implies there exists rational a,c
s.t. a<c and c<b
R
This symbol represents the set of real numbers.
S \subset R and exists y in R : forall x in S x <= y) implies
exists z in R such that
(( forall x in S x <= z) and
((forall x in S x <= w) implies z <= w)
C
This symbol represents the set of complex numbers.
for all z | if z is complex then there exist reals x,y
s.t. z = x + i * y