multiset1 http://www.openmath.org/cd/multiset1.ocd 2003-04-01 2001-03-12 2 0 official logic1 quant1 relation1 This CD defines the set functions and constructors for basic multiset theory. It is intended to be `compatible' with the corresponding elements in MathML i.e. set operations acting on sets of type=multiset. Based on set1.ocd size This symbol is used to denote the number of elements in a multiset. It is either a non-negative integer, or an infinite cardinal number. The symbol infinity may be used for an unspecified infinite cardinal. The size of the multiset{3,3,9} = 3 3 3 9 3 cartesian_product This symbol represents an n-ary construction function for constructing the Cartesian product of multisets. It takes n multiset arguments in order to construct their Cartesian product. An example to show the representation of the Cartesian product of multisets: AxBxC. emptyset This symbol is used to represent the empty multiset, that is the multiset which contains no members. It takes no parameters. The intersection of A with the empty (multi) set is the empty (multi) set The union of A with the empty (multi) set is A multiset This symbol represents the multiset construct. It is either an n-ary function, in which case the multiset entries are given explicitly, or it works on an elements construct. There is no implied ordering to the elements of a multiset. The multiset {4, 1, 0, 1 4} 4 1 0 1 4 intersect This symbol is used to denote the n-ary intersection of multisets. It takes multisets as arguments, and denotes the multiset that contains all the elements that occur in all of them, with multiplicity the minimum of their multiplicities in all multisets. (A intersect B) is a subset of A and (A intersect B) is a subset of B union This symbol is used to denote the n-ary union of multisets. It takes multisets as arguments, and denotes the multiset that contains all the elements that occur in any of them, with multiplicity the sum of all the multiplicities in the multiset arguments. A is a subset of (A union B) and B is a subset of (A union B) for all sets A,B and C union(A,intersect(B,C)) = intersect(union(A,B),union(A,C)) setdiff This symbol is used to denote the multiset difference of two multisets. It takes two multisets as arguments, and denotes the multiset that contains all the elements that occur in the first multiset with strictly greater multiplicity than in the second. The multiplicity in the result is the difference of the two. the difference of A and B is a subset of A subset This symbol has two (multiset) arguments. It is used to denote that the first set is a subset of the second, i.e. every element of the first occurs with multiplicity at least as much in the second. if B is a subset of A and C is a subset of B then C is a subset of A in This symbol has two arguments, an element and a multiset. It is used to denote that the element is in the given multiset. if a is in A and a is in B then a is in A intersection B notin This symbol has two arguments, an element and a multiset. It is used to denote that the element is not in the given multiset. 4 is not in {1,1,2,3} 4 1 1 2 3 prsubset This symbol has two (multiset) arguments. It is used to denote that the first multiset is a proper subset of the second, that is a subset of the second multiset but not actually equal to it. {2,3} is a proper subset of {2,2,3} 2 3 2 2 3 notsubset This symbol has two (multiset) arguments. It is used to denote that the first multiset is not a subset of the second. {2,3,3} is not a subset of {1,2,3} 2 3 3 1 2 3 notprsubset This symbol has two (multiset) arguments. It is used to denote that the first multiset is not a proper subset of the second. A proper subset of a multiset is a subset of the multiset but not actually equal to it. {1,2,1} is not a proper subset of {1,2,1} 1 2 1 1 2 1