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

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.