Journal of Formalized Mathematics
Volume 1, 1989
University of Bialystok
Copyright (c) 1989
Association of Mizar Users
Functions and Their Basic Properties

Czeslaw Bylinski

Warsaw University, Bialystok

Supported by RPBP.III24.C1.
Summary.

The definitions of the mode Function and the graph of a function
are introduced. The graph of a function is defined to be
identical with the function.
The following concepts are also defined: the domain of a function, the range of
a function, the identity function, the composition of functions,
the 11 function, the inverse function, the restriction of
a function, the image and the inverse image.
Certain basic facts about
functions and the notions defined in the article are proved.
MML Identifier:
FUNCT_1
The terminology and notation used in this paper have been
introduced in the following articles
[1]
[2]
Contents (PDF format)
Bibliography
 [1]
Andrzej Trybulec.
Tarski Grothendieck set theory.
Journal of Formalized Mathematics,
Axiomatics, 1989.
 [2]
Edmund Woronowicz.
Relations and their basic properties.
Journal of Formalized Mathematics,
1, 1989.
Received March 3, 1989
[
Download a postscript version,
MML identifier index,
Mizar home page]