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.III-24.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 non-empty 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.

#### MML Identifier: FUNCOP_1

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.