Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990
Association of Mizar Users
Function Domains and Fr\aenkel Operator

Andrzej Trybulec

Warsaw University, Bialystok

Supported by RPBP.III24.C1.
Summary.

We deal with
a nonempty set of functions and a nonempty set of functions
from a set $A$ to a nonempty set $B$.
In the case when $B$ is a nonempty set, $B^A$ is redefined.
It yields a nonempty set of functions from $A$ to $B$.
An element of such a set is redefined as a function from $A$ to $B$.
Some theorems concerning these concepts are proved, as well as
a number
of schemes dealing with infinity and the Axiom of Choice. The article
contains a number of schemes allowing for simple logical transformations
related to terms constructed with the Fr{\ae}nkel Operator.
The terminology and notation used in this paper have been
introduced in the following articles
[6]
[3]
[8]
[9]
[4]
[7]
[1]
[2]
[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.
Some basic properties of sets.
Journal of Formalized Mathematics,
1, 1989.
 [4]
Agata Darmochwal.
Finite sets.
Journal of Formalized Mathematics,
1, 1989.
 [5]
Andrzej Trybulec.
Semilattice operations on finite subsets.
Journal of Formalized Mathematics,
1, 1989.
 [6]
Andrzej Trybulec.
Tarski Grothendieck set theory.
Journal of Formalized Mathematics,
Axiomatics, 1989.
 [7]
Andrzej Trybulec and Agata Darmochwal.
Boolean domains.
Journal of Formalized Mathematics,
1, 1989.
 [8]
Zinaida Trybulec.
Properties of subsets.
Journal of Formalized Mathematics,
1, 1989.
 [9]
Edmund Woronowicz.
Relations and their basic properties.
Journal of Formalized Mathematics,
1, 1989.
Received February 7, 1990
[
Download a postscript version,
MML identifier index,
Mizar home page]