logo

Theory of proveit.logic.sets

Basic set theory theory dealing with membership (e.g., $x \in S$), enumeration (e.g., $\{e_1, e_2, e_3\}$), containment (e.g., $A \subseteq B$), unification (e.g., $A \cup B \cup C$), intersection (e.g., $A \cap B \cap C$), subtraction (e.g., $A - B$), comprehension (e.g., $\{f(x)~|~Q(x)\}_{x \in S}$), and cardinatly (e.g., $|S|$).

In [1]:
import proveit
%theory

Local content of this theory

common expressions axioms theorems demonstrations

Sub-theories

membershipIs an element a member of a set? Not a member of a set?
equivalenceDo sets have the same elements?
enumerationDefine a set by enumerating its contents.
inclusionIs one set included in another (as a subset)?
unificationDefine a set as the union of sets.
intersectionDefine a set as the intersection of sets.
subtractionDefine a set by removing elements from an original set.
comprehensionDefine a set according to the properties of its members.
power_setDefine a set as the power set of another set.
disjointnessAre there common elements between sets? Also defines "distinct".
cardinalityHow large is a set?

All axioms contained within this theory

This theory contains no axioms directly.

proveit.logic.sets.membership

proveit.logic.sets.equivalence

proveit.logic.sets.enumeration

proveit.logic.sets.inclusion

proveit.logic.sets.unification

proveit.logic.sets.intersection

proveit.logic.sets.subtraction

proveit.logic.sets.comprehension

proveit.logic.sets.power_set

proveit.logic.sets.disjointness

proveit.logic.sets.cardinality