logo

Context: proveit.logic.set_theory.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
%context