# 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