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

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 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
In [2]:
%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
In [3]:
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):

In [4]:
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.

In [5]:
injection_is_function = Forall(
    (A, B), Forall(f, InSet(f, Functions(A, B)),
                   domain=Injections(A, B)))
injection_is_function (conjecture without proof):

In [6]:
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):

In [7]:
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

In [8]:
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):

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