Journal of Formalized Mathematics
Volume 1, 1989
University of Bialystok
Copyright (c) 1989
Association of Mizar Users
Functions from a Set to a Set

Czeslaw Bylinski

Warsaw University, Bialystok

Supported by RPBP.III24.C1.
Summary.

The article is a continuation of [1].
We define the following concepts:
a function from a set $X$ into a set $Y$, denoted by ``Function of $X$,$Y$'',
the set of all functions from a set $X$ into a set $Y$, denoted by Funcs($X$,$Y$),
and the permutation of a set (mode Permutation of $X$, where $X$ is a set).
Theorems and schemes included in the article are reformulations of the
theorems of [1] in the new terminology.
Also some basic facts about functions of two variables are proved.
MML Identifier:
FUNCT_2
The terminology and notation used in this paper have been
introduced in the following articles
[4]
[3]
[5]
[6]
[7]
[1]
[2]

Functions from a set to a set

Partial functions from a set to a set (from \cite{PARTFUN1.ABS})
Bibliography
 [1]
Czeslaw Bylinski.
Functions and their basic properties.
Journal of Formalized Mathematics,
1, 1989.
 [2]
Czeslaw Bylinski.
Partial functions.
Journal of Formalized Mathematics,
1, 1989.
 [3]
Czeslaw Bylinski.
Some basic properties of sets.
Journal of Formalized Mathematics,
1, 1989.
 [4]
Andrzej Trybulec.
Tarski Grothendieck set theory.
Journal of Formalized Mathematics,
Axiomatics, 1989.
 [5]
Zinaida Trybulec.
Properties of subsets.
Journal of Formalized Mathematics,
1, 1989.
 [6]
Edmund Woronowicz.
Relations and their basic properties.
Journal of Formalized Mathematics,
1, 1989.
 [7]
Edmund Woronowicz.
Relations defined on sets.
Journal of Formalized Mathematics,
1, 1989.
Received April 6, 1989
[
Download a postscript version,
MML identifier index,
Mizar home page]