logo

Theorems for context proveit.logic.set_theory

In [1]:
from proveit.logic import Forall, NotInSet, EmptySet
from proveit._common_ import x
%begin theorems
Defining theorems for context 'proveit.logic.set_theory'
Subsequent end-of-cell assignments will define theorems
'%end theorems' will finalize the definitions

Nothing is in the empty set (everything is not in the empty set):

In [2]:
allNotInEmpty = Forall(x, NotInSet(x, EmptySet))
Out[2]:
In [3]:
%end theorems
Theorems may be imported from autogenerated _theorems_.py