Theory of proveit.logic.sets.enumeration

Enumeration provides a simple way to define a finite set via enumerating the containing elements. For example, $S = \{e_1, e_2, e_3\}$, is the set containing only $e_1$, $e_2$, and $e_3$. That is, $x \in S$ if $x=e_1$ or $x=e_2$ or $x=e_3$; otherwise, $x \notin S$.

In [1]:
import proveit

Local content of this theory

All axioms contained within this theory