logo

Theorems (or conjectures) for the theory of proveit.logic.classes.membership

In [1]:
import proveit
# Prepare this notebook for defining the theorems of a theory:
%theorems_notebook # Keep this at the top following 'import proveit'.

from proveit import x, C
from proveit.logic import (
    Forall, Not, in_bool, Equals, InClass, NotInClass)
In [2]:
%begin theorems

Defining theorems for theory 'proveit.logic.classes.membership'
Subsequent end-of-cell assignments will define theorems
'%end theorems' will finalize the definitions
In [3]:
not_in_class_is_bool = Forall(
    (x, C), in_bool(NotInClass(x, C)), 
    conditions=[in_bool(InClass(x, C))] )
not_in_class_is_bool (conjecture without proof):
In [4]:
unfold_not_in_class = Forall(
    (x, C), Not(InClass(x, C)), conditions=[NotInClass(x, C)])
unfold_not_in_class (conjecture without proof):
In [5]:
fold_not_in_class = Forall(
    (x, C), NotInClass(x, C), conditions=[Not(InClass(x, C))])
fold_not_in_class (conjecture without proof):
In [6]:
%end theorems

These theorems may now be imported from the theory package: proveit.logic.classes.membership