[Next] [Prev] [Right] [Left] [Up] [Index] [Root]
Operations on Sets

### Operations on Sets

#### Boolean Functions and Operators

As explained in the Introduction, when elements are taken out of a set their parent will be the universe of the set (or, if the universe is itself a set, the universe of the universe, etc.); in particular, the set itself is not the parent. Hence equality testing on set elements is in fact equality testing between two elements of certain algebraic structures, and the sets are irrelevant. We only list the (in)equality operator for convenience here.

Element membership testing is of critical importance for all types of sets.

Testing whether or not R is a subset of S can be done if R is an enumerated or indexed set and S is any set; hence (in)equality testing is only possible between sets that are not formal sets.

##### IsNull(R) : SetEnum -> BoolElt
Returns true if and only if the enumerated or indexed set R is empty and does not have its universe defined.
##### IsEmpty(R) : SetEnum -> BoolElt
Returns true if and only if the enumerated or indexed set R is empty.
##### x eq y : Elt, Elt -> BoolElt
Given an element x of a set R with universe U and an element y of a set S with universe V, where a common overstructure W can be found with U subset W supset V (see the Introduction for details on overstructures), return true if and only if x and y are equal as elements of W.

##### x ne y : Elt, Elt -> BoolElt
Given an element x of a set R with universe U and an element y of a set S with universe V, where a common overstructure W can be found with U subset W supset V (see the Introduction for details on overstructures), return true if and only if x and y are distinct as elements of W.
##### x in R : Elt, Set -> BoolElt
True if and only if the element x is a member of the set R. If x is not an element of the universe U of R, it is attempted to coerce x into U; if this fails, an error occurs.
##### x notin R : Elt, Set -> BoolElt
True if and only if the element x is not a member of the set R. If x is not an element of the parent structure U of R, it is attempted to coerce x into U; if this fails, an error occurs.
##### R subset S : SetIndx, Set -> BoolElt
True if the enumerated or indexed set R is a subset of the set S, false otherwise. Coercion of the elements of R into S is attempted if necessary, and an error occurs if this fails.
##### R notsubset S : SetIndx, Set -> BoolElt
True if the enumerated or indexed set R is a not a subset of the set S, false otherwise. Coercion of the elements of R into S is attempted if necessary, and an error occurs if this fails.
##### R eq S : SetIndx, SetEnum -> BoolElt
True if and only if R and S are identical sets, where R and S are enumerated or indexed sets; the index function is irrelevant for deciding equality. Coercion of the elements of R into S is attempted if necessary, and an error occurs if this fails.
##### R ne S : SetIndx, SetEnum -> BoolElt
True if and only if R and S are distinct sets, where R and S are enumerated or indexed sets; the index function is irrelevant for deciding equality. Coercion of the elements of R into S is attempted if necessary, and an error occurs if this fails.

#### Binary Set Operators

For each of the following operators, R and S are either both formal sets or both enumerated sets. If R and S are both formal sets, then an error will occur unless both have been constructed with the same carrier structure F in the definition. If R and S are both enumerated sets, then an error occurs unless the universes of R and S are compatible, as defined in the Introduction to this Part.

Note that

```Q := { ! x in R !}
```
converts an enumerated set R into a formal set Q.
##### R join S : SetForm, SetForm -> SetForm
Union of the sets R and S (see above for the restrictions on R and S).
##### R meet S : SetForm, SetForm -> SetForm
Intersection of the sets R and S (see above for the restrictions on R and S).
##### R diff S : SetForm, SetForm -> SetForm
Difference of the sets R and S, i.e., the set consisting of those elements of R which are not members of S (see above for the restrictions on R and S).
##### R sdiff S : SetForm, SetForm -> SetForm
Symmetric difference of the sets R and S, i.e., the set consisting of those elements which are members of either R or S but not both (see above for the restrictions on R and S).

### Example Set_Join (H4E10)

```> R := { 1, 2, 3 };
> S := { 1, 1/2, 1/3 };
> print R join S;
{ 1/3, 1/2, 1, 2, 3 }
> print R meet S;
{ 1 }
> print R diff S;
{ 2, 3 }
> print S diff R;
{ 1/3, 1/2 }
> print R sdiff S;
{ 1/3, 1/2, 2, 3 }
```

[Next] [Prev] [Right] [Left] [Up] [Index] [Root]