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

Contents (PDF format)

1. Properties of Cartesian product
2. Curried and uncurried functions of some functions
3. Functions yielding functions
4. Cartesian product of functions with the same domain
5. Cartesian product of functions
6. 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.