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.III-24.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 1-1 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]