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

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

%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

membership_unfolding = Forall(
    (A, B), Forall(
        f, And(InSet(f, Injections(A, B)),
                   InSet(f, Surjections(A, B))),
        domain=Bijections(A, B)))

membership_unfolding (conjecture without proof):

membership_folding = Forall(
    (A, B), Forall(
        f, InSet(f, Bijections(A, B)),
        conditions=[InSet(f, Injections(A, B)),
                    InSet(f, Surjections(A, B))]))

membership_folding (conjecture without proof):

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

bijection_is_function = Forall(
    (A, B), Forall(f, InSet(f, Functions(A, B)),
                   domain=Bijections(A, B)))

bijection_is_function (conjecture without proof):

bijection_is_injection = Forall(
    (A, B), Forall(f, InSet(f, Injections(A, B)),
                   domain=Bijections(A, B)))

bijection_is_injection (conjecture without proof):

bijection_is_surjection = Forall(
    (A, B), Forall(f, InSet(f, Surjections(A, B)),
                   domain=Bijections(A, B)))

bijection_is_surjection (conjecture without proof):

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))))

elim_domain_condition (conjecture without proof):

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

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)))))

bijective_by_uniqueness (conjecture without proof):

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())

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.

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)

bijective_by_finite_image_size (conjecture without proof):

%end theorems

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