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 cardinality (e.g., $|S|$).

import proveit
%theory

membership	Is an element a member of a set? Not a member of a set?
equivalence	Do sets have the same elements?
enumeration	Define a set by enumerating its contents.
inclusion	Is one set included in another (as a subset)?
unification	Define a set as the union of sets.
intersection	Define a set as the intersection of sets.
subtraction	Define a set by removing elements from an original set.
comprehension	Define a subset according to the properties of its members.
power_set	Define a set as the power set of another set.
cartesian_products	Define a set as all combinations of elements of other sets.
disjointness	Are there common elements between sets? Also defines "distinct".
cardinality	How large is a set?
functions	A function is a mapping from a domain to a codomain (both sets) and has various properties.

Theory of proveit.logic.sets¶

Local content of this theory

Sub-theories

All axioms contained within this theory

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.cartesian_products

proveit.logic.sets.disjointness

proveit.logic.sets.cardinality

proveit.logic.sets.functions