set3
http://www.openmath.org/cd/set3.ocd
2003-04-01
1999-05-10
1
1
experimental
relation1
set1
nums1
setname1
This CD defines more set functions.
big_intersect
This symbol is a unary function whose argument should be a collection C of
subsets of a given set. When applied to C, it represents the intersection
over all members of C.
big_union
This symbol is a unary function whose argument should be a collection C of
subsets of a given set. When applied to C, it represents the union over all members of C.
cartesian_power
This symbol is a binary function whose first argument should be a set A and
whose second argument should be a natural number k.
When applied to A and k, it represents the Cartesian product of k copies of A.
powerset
This symbol represents unary function whose argument should be a set.
When applied to a set X, it represents the collection of all subsets of X.
The intersection over all subsets of a given set X is the empty set.
k_subsets
This symbol represents a binary function whose first argument should be a set
and whose second argument should be a natural number.
When applied to a set X and a number k, it represents the collection of all subsets of X of
size k.
map_with_target
This symbol represents a function with three arguments.
The first argument is a function assignment f (in the form of a lambda
binding),
the second argument is a set X on which the first argument f is defined.
The third argument specifies the range Y of the function.
The symbol is used to denote the image {f(x) in Y | x in X} of application of the
function f on the elements of X (so as to form a subset of Y).
One may form a set in the following way. This gives the set {1^2, 2^2,
... , 10^2 }
2
1 10
The definition of a product of subsets X and Y of a group G:
map_with_condition
This symbol represents a function with three arguments.
The first argument is a function assignment f (in the form of a lambda
binding),
the second argument is a set X.
The third argument specifies a Boolean function P on X defining the subset Z of X
(so Z = {x in X| P(x)}) on which the first argument f is defined,
The symbol is used to denote the image {f(x) | x in X and P(x)} of application of the
function f on the elements of Z.
One may form a set in the following way. This gives the set {2^2, 4^2,
... , 10^2 }
2
1 10
2
map_with_target_and_condition
This symbol represents a function with four arguments.
The first argument is a function assignment f (in the form of a lambda
binding),
the second argument is a set X on which the first argument f is defined.
The third argument specifies the range Y of the function.
The fourth argument specifies a Boolean function P on X defining the subset Z of X
(so Z = {x in X| P(x)}) on which the first argument f is defined,
The symbol is used to denote the image {f(x) in Y | x in X and P(x)} of application of the
function f on the elements of Z.
One may form a set in the following way. This gives the set {1^2, 2^2,
... , 10^2 }
2
1 10
2