Theory of proveit.logic.sets.disjointness¶
The Disjoint operation defines a property for a collection of sets. It evaluates to TRUE if and only if the sets are mutually/pairwise disjoint; that is, the intersection of any two of the sets is the empty set. We define this property to be True when given zero or one set (there are no pairs of sets, so all pairs are vacuously disjoint).
The Distinct operation defines a property for any collection. It evaluates to TRUE if and only if the elements are all unique; that is, any pair of the given elements are not equal to each other.
