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         

Contents (PDF format)

#### Bibliography

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