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

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 a, b, f, n, x, A, B, C, fa, fb, fx
from proveit import Lambda, Conditional
from proveit.logic import (
    And, Forall, Equals, NotEquals, InSet, Surjections)

%begin theorems

Defining theorems for theory 'proveit.logic.sets.functions.surjections'
Subsequent end-of-cell assignments will define theorems
'%end theorems' will finalize the definitions

elim_domain_condition = Forall(
    (A, B), Forall(f, InSet(f, Surjections(A, B)),
                   condition=InSet(Lambda(x, Conditional(fx, InSet(x, A))),
                                   Surjections(A, B))))

elim_domain_condition (conjecture without proof):

%end theorems

These theorems may now be imported from the theory package: proveit.logic.sets.functions.surjections