Theorems (or conjectures) for the theory of proveit.logic.sets.functions

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 Lambda, Conditional
from proveit import f, x, A, B, fx
from proveit.logic import Forall, Equals, InSet
from proveit.logic.sets import Functions
In [2]:
%begin theorems
Defining theorems for theory 'proveit.logic.sets.functions'
Subsequent end-of-cell assignments will define theorems
'%end theorems' will finalize the definitions
In [3]:
membership_unfolding = Forall(
    (A, B), Forall(f, Forall(x, InSet(fx, B), domain=A),
                   domain=Functions(A, B)))
membership_unfolding (conjecture without proof):

In [4]:
membership_folding = Forall(
    (A, B), Forall(f, InSet(f, Functions(A, B)),
                   condition=Forall(x, InSet(fx, B), domain=A)))
membership_folding (conjecture without proof):

In [5]:
elim_domain_condition = Forall(
    (A, B), Forall(f, InSet(f, Functions(A, B)),
                   condition=InSet(Lambda(x, Conditional(fx, InSet(x, A))),
                                   Functions(A, B))))
elim_domain_condition (conjecture without proof):

In [6]:
%end theorems
These theorems may now be imported from the theory package: proveit.logic.sets.functions