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

import proveit
%theory

Local content of this theory

common expressions	axioms	theorems	demonstrations

Sub-theories

All axioms contained within this theory

proveit.logic.sets.enumeration.enum_set_def

proveit.logic.sets.enumeration.empty_set_def