logo

Axioms for context proveit.logic.set_theory

In [1]:
from proveit.logic import EmptySet, Set, Equals
%begin axioms
Defining axioms for context 'proveit.logic.set_theory'
Subsequent end-of-cell assignments will define axioms
%end_axioms will finalize the definitions

Identify the empty set, $\emptyset$, with the empty enumeration, $\{\}$:

In [2]:
enumEmpty = Equals(EmptySet, Set())
Out[2]:
enumEmpty:
In [3]:
%end axioms
Axioms may be imported from autogenerated _axioms_.py