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) : SetIndx -> BoolElt
Returns true if and only if the enumerated or indexed set R is empty and does not have its universe defined.
Returns true if and only if the enumerated or indexed set R is empty.
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.
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.
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.
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.
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.
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.
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.
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.
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.
Union of the sets R and S (see above for the restrictions on R and S).
Intersection of the sets R and S (see above for the restrictions on R and S).
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).
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).
> 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 }