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

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, Disjoint, SubsetEq,
    Functions, Image, Injections)
from proveit.numbers import Natural

%begin theorems

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

membership_unfolding = Forall(
    (A, B), Forall(
        f, And(InSet(f, Functions(A, B)),
               Forall((a, b), NotEquals(fa, fb),
                      domain=A, condition=NotEquals(a, b))),
        domain=Injections(A, B)))

membership_unfolding (conjecture without proof):

membership_folding = Forall(
    (A, B), Forall(
        f,  InSet(f, Injections(A, B)),
        domain=Functions(A, B),
        condition=Forall((a, b), NotEquals(fa, fb),
                         domain=A, condition=NotEquals(a, b))))

membership_folding (conjecture without proof):

An injection is a function.

injection_is_function = Forall(
    (A, B), Forall(f, InSet(f, Functions(A, B)),
                   domain=Injections(A, B)))

injection_is_function (conjecture without proof):

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

elim_domain_condition (conjecture without proof):

subset_injection = Forall(
    (A, B, C), Forall(f, InSet(f, Injections(A, C)),
                      domain = Injections(B, C)),
    condition=SubsetEq(A, B))

subset_injection (conjecture without proof):

Useful properties of injections

disjoint_set_images_are_disjoint = Forall(
    (A, B, C), Forall(
        f, Disjoint(Image(f, A), Image(f, B)),
        domain = Injections(A, C)),
    condition = Disjoint(A, B))

disjoint_set_images_are_disjoint (conjecture without proof):

%end theorems

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