Journal of Formalized Mathematics
Volume 3, 1991
University of Bialystok
Copyright (c) 1991
Association of Mizar Users
Cartesian Product of Functions
-
Grzegorz Bancerek
-
Warsaw University, Bialystok
Summary.
-
A supplement of [3] and [2],
i.e. some useful and explanatory properties of the product and also
the curried and uncurried functions are shown. Besides, the functions yielding
functions are considered: two different products and other operation of
such functions are
introduced. Finally, two facts are presented: quasi-distributivity of
the power of the set to other one w.r.t. the union
($X^{\biguplus_{x}f(x)} \approx \prod_{x}X^{f(x)}$) and
quasi-distributivity of the product w.r.t. the raising to the power
($\prod_{x}{f(x)^X} \approx (\prod_{x}f(x))^X$).
MML Identifier:
FUNCT_6
The terminology and notation used in this paper have been
introduced in the following articles
[16]
[15]
[9]
[17]
[18]
[6]
[4]
[13]
[7]
[8]
[5]
[1]
[14]
[10]
[11]
[2]
[12]
[3]
-
Properties of Cartesian product
-
Curried and uncurried functions of some functions
-
Functions yielding functions
-
Cartesian product of functions with the same domain
-
Cartesian product of functions
-
Function yielding powers
Bibliography
- [1]
Grzegorz Bancerek.
Zermelo theorem and axiom of choice.
Journal of Formalized Mathematics,
1, 1989.
- [2]
Grzegorz Bancerek.
Curried and uncurried functions.
Journal of Formalized Mathematics,
2, 1990.
- [3]
Grzegorz Bancerek.
K\"onig's theorem.
Journal of Formalized Mathematics,
2, 1990.
- [4]
Grzegorz Bancerek and Krzysztof Hryniewiecki.
Segments of natural numbers and finite sequences.
Journal of Formalized Mathematics,
1, 1989.
- [5]
Czeslaw Bylinski.
Basic functions and operations on functions.
Journal of Formalized Mathematics,
1, 1989.
- [6]
Czeslaw Bylinski.
Functions and their basic properties.
Journal of Formalized Mathematics,
1, 1989.
- [7]
Czeslaw Bylinski.
Functions from a set to a set.
Journal of Formalized Mathematics,
1, 1989.
- [8]
Czeslaw Bylinski.
Partial functions.
Journal of Formalized Mathematics,
1, 1989.
- [9]
Czeslaw Bylinski.
Some basic properties of sets.
Journal of Formalized Mathematics,
1, 1989.
- [10]
Czeslaw Bylinski.
Finite sequences and tuples of elements of a non-empty sets.
Journal of Formalized Mathematics,
2, 1990.
- [11]
Czeslaw Bylinski.
The modification of a function by a function and the iteration of the composition of a function.
Journal of Formalized Mathematics,
2, 1990.
- [12]
Andrzej Nedzusiak.
$\sigma$-fields and probability.
Journal of Formalized Mathematics,
1, 1989.
- [13]
Beata Padlewska.
Families of sets.
Journal of Formalized Mathematics,
1, 1989.
- [14]
Andrzej Trybulec.
Binary operations applied to functions.
Journal of Formalized Mathematics,
1, 1989.
- [15]
Andrzej Trybulec.
Enumerated sets.
Journal of Formalized Mathematics,
1, 1989.
- [16]
Andrzej Trybulec.
Tarski Grothendieck set theory.
Journal of Formalized Mathematics,
Axiomatics, 1989.
- [17]
Zinaida Trybulec.
Properties of subsets.
Journal of Formalized Mathematics,
1, 1989.
- [18]
Edmund Woronowicz.
Relations and their basic properties.
Journal of Formalized Mathematics,
1, 1989.
Received September 30, 1991
[
Download a postscript version,
MML identifier index,
Mizar home page]