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

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 f, g, n, x, y, A, B, C, fx, fy, gx
from proveit import Function, Lambda, Conditional
from proveit.relation import total_ordering
from proveit.logic import (
And, Implies, Forall, Equals, NotEquals, InSet, Card,
Functions, Image, Bijections, Injections, Surjections)
from proveit.numbers import Natural
In [2]:
%begin theorems
Defining theorems for theory 'proveit.logic.sets.functions.bijections'
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, Injections(A, B)),
InSet(f, Surjections(A, B))),
domain=Bijections(A, B)))
Out[3]:
membership_unfolding (conjecture without proof):

In [4]:
membership_folding = Forall(
(A, B), Forall(
f, InSet(f, Bijections(A, B)),
conditions=[InSet(f, Injections(A, B)),
InSet(f, Surjections(A, B))]))
Out[4]:
membership_folding (conjecture without proof):

A bijection is a function, an injection, and a surjection.

In [5]:
bijection_is_function = Forall(
(A, B), Forall(f, InSet(f, Functions(A, B)),
domain=Bijections(A, B)))
Out[5]:
bijection_is_function (conjecture without proof):

In [6]:
bijection_is_injection = Forall(
(A, B), Forall(f, InSet(f, Injections(A, B)),
domain=Bijections(A, B)))
Out[6]:
bijection_is_injection (conjecture without proof):

In [7]:
bijection_is_surjection = Forall(
(A, B), Forall(f, InSet(f, Surjections(A, B)),
domain=Bijections(A, B)))
Out[7]:
bijection_is_surjection (conjecture without proof):

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

If mapped unique elements of a function are unique, then the function is a bijection onto its image.

In [9]:
bijective_by_uniqueness = Forall(
(f, A),
Implies(Forall((x, y), NotEquals(fx, fy),
domain=A, condition=NotEquals(x, y)),
InSet(f, Bijections(A, Image(f, A)))))
Out[9]:
bijective_by_uniqueness (conjecture without proof):

In [10]:
bijection_transitivity = Forall(
(f, g, A, B, C),
Implies(And(InSet(f, Bijections(A, B)), InSet(g, Bijections(B, C))),
InSet(Lambda(x, Conditional(Function(g, fx), InSet(x, A))),
Bijections(A, C)))
.with_wrap_before_operator())
Out[10]:
bijection_transitivity (conjecture without proof):

If the domain is finite, we know the function is a bijection if its image covers the codomain and is the same size as the domain.

In [11]:
bijective_by_finite_image_size = Forall(
n, Forall(
(f, A), InSet(f, Bijections(A, Image(f, A))),
condition=total_ordering(
Equals(Card(Image(f, A)), Card(A)),
Equals(Card(A), n))),
domain=Natural)
Out[11]:
bijective_by_finite_image_size (conjecture without proof):

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