Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990 Association of Mizar Users

The Modification of a Function by a Function and the Iteration of the Composition of a Function


Czeslaw Bylinski
Warsaw University, Bialystok
Supported by RPBP.III-24.C1.

Summary.

In the article we introduce some operations on functions. We define the natural ordering relation on functions. The fact that a function $f$ is less than a function $g$ we denote by $f \leq g$ and we define by $\hbox{graph} f \subseteq \hbox{graph} f$. In the sequel we define the modifications of a function $f$ by a function $g$ denoted $f \hbox{+$\cdot$} g$ and the $n$-th iteration of the composition of a function $f$ denoted by $f^n$. We prove some propositions related to the introduced notions.

MML Identifier: FUNCT_4

The terminology and notation used in this paper have been introduced in the following articles [6] [4] [7] [8] [1] [9] [2] [3] [5]

Contents (PDF format)

Bibliography

[1] Czeslaw Bylinski. Functions and their basic properties. Journal of Formalized Mathematics, 1, 1989.
[2] Czeslaw Bylinski. Functions from a set to a set. Journal of Formalized Mathematics, 1, 1989.
[3] Czeslaw Bylinski. Partial functions. Journal of Formalized Mathematics, 1, 1989.
[4] Czeslaw Bylinski. Some basic properties of sets. Journal of Formalized Mathematics, 1, 1989.
[5] Andrzej Trybulec. Binary operations applied to functions. Journal of Formalized Mathematics, 1, 1989.
[6] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.
[7] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.
[8] Edmund Woronowicz. Relations and their basic properties. Journal of Formalized Mathematics, 1, 1989.
[9] Edmund Woronowicz. Relations defined on sets. Journal of Formalized Mathematics, 1, 1989.

Received March 1, 1990


[ Download a postscript version, MML identifier index, Mizar home page]