Journal of Formalized Mathematics
Volume 1, 1989
University of Bialystok
Copyright (c) 1989
Association of Mizar Users
Binary Operations Applied to Functions

Andrzej Trybulec

Warsaw University, Bialystok

Supported by RPBP.III24.C1.
Summary.

In the article we introduce functors yielding to a binary operation
its composition with an arbitrary functions on its left side, its right
side or both. We prove theorems describing the basic properties of these
functors. We introduce also constant functions and converse of a function.
The recent concept is defined for an arbitrary function, however is
meaningful in the case of functions which range is a subset of a Cartesian
product of two sets. Then the converse of a function has the same domain
as the function itself and assigns to an element of the domain the mirror
image of the ordered pair assigned by the function.
In the case of functions defined on a nonempty set we redefine
the above mentioned functors and prove simplified versions of theorems proved
in the general case. We prove also theorems stating relationships between
introduced concepts and such properties of binary operations as
commutativity or associativity.
The terminology and notation used in this paper have been
introduced in the following articles
[7]
[6]
[9]
[8]
[11]
[10]
[3]
[5]
[4]
[1]
[2]
Contents (PDF format)
Bibliography
 [1]
Czeslaw Bylinski.
Basic functions and operations on functions.
Journal of Formalized Mathematics,
1, 1989.
 [2]
Czeslaw Bylinski.
Binary operations.
Journal of Formalized Mathematics,
1, 1989.
 [3]
Czeslaw Bylinski.
Functions and their basic properties.
Journal of Formalized Mathematics,
1, 1989.
 [4]
Czeslaw Bylinski.
Functions from a set to a set.
Journal of Formalized Mathematics,
1, 1989.
 [5]
Czeslaw Bylinski.
Partial functions.
Journal of Formalized Mathematics,
1, 1989.
 [6]
Czeslaw Bylinski.
Some basic properties of sets.
Journal of Formalized Mathematics,
1, 1989.
 [7]
Andrzej Trybulec.
Tarski Grothendieck set theory.
Journal of Formalized Mathematics,
Axiomatics, 1989.
 [8]
Andrzej Trybulec.
Tuples, projections and Cartesian products.
Journal of Formalized Mathematics,
1, 1989.
 [9]
Zinaida Trybulec.
Properties of subsets.
Journal of Formalized Mathematics,
1, 1989.
 [10]
Edmund Woronowicz.
Relations and their basic properties.
Journal of Formalized Mathematics,
1, 1989.
 [11]
Edmund Woronowicz.
Relations defined on sets.
Journal of Formalized Mathematics,
1, 1989.
Received September 4, 1989
[
Download a postscript version,
MML identifier index,
Mizar home page]