Introduction to Theory of Rearrangement

Yuji Sakai

Shinshu University, Nagano

Jaroslaw Kotowicz

Warsaw University, Bialystok

Summary.

An introduction to the rearrangement theory for finite functions (e.g. with the finite domain and codomain). The notion of generators and cogenerators of finite sets (equivalent to the order in the language of finite sequences) has been defined. The notion of rearrangement for a function into finite set is presented. Some basic properties of these notions have been proved.

Dedicated to Professor Tsuyoshi Ando on his sixtieth birthday.

MML Identifier: REARRAN1

Contents (PDF format)

Bibliography

[1] Grzegorz Bancerek. Cardinal numbers. Journal of Formalized Mathematics, 1, 1989.

[2] Grzegorz Bancerek. The fundamental properties of natural numbers. Journal of Formalized Mathematics, 1, 1989.

[3] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Journal of Formalized Mathematics, 1, 1989.

[4] Czeslaw Bylinski. Functions and their basic properties. Journal of Formalized Mathematics, 1, 1989.

[5] Czeslaw Bylinski. Partial functions. Journal of Formalized Mathematics, 1, 1989.

[6] Czeslaw Bylinski. Some basic properties of sets. Journal of Formalized Mathematics, 1, 1989.

[7] Czeslaw Bylinski. Binary operations applied to finite sequences. Journal of Formalized Mathematics, 2, 1990.

[8] Czeslaw Bylinski. The sum and product of finite sequences of real numbers. Journal of Formalized Mathematics, 2, 1990.

[9] Agata Darmochwal. Finite sets. Journal of Formalized Mathematics, 1, 1989.

[10] Agata Darmochwal and Yatsuka Nakamura. The topological space $\calE^2_\rmT$. Arcs, line segments and special polygonal arcs. Journal of Formalized Mathematics, 3, 1991.

[11] Krzysztof Hryniewiecki. Basic properties of real numbers. Journal of Formalized Mathematics, 1, 1989.

[12] Jaroslaw Kotowicz. Real sequences and basic operations on them. Journal of Formalized Mathematics, 1, 1989.

[13] Jaroslaw Kotowicz. Partial functions from a domain to the set of real numbers. Journal of Formalized Mathematics, 2, 1990.

[14] Jaroslaw Kotowicz. Functions and finite sequences of real numbers. Journal of Formalized Mathematics, 5, 1993.

[15] Jaroslaw Kotowicz and Yuji Sakai. Properties of partial functions from a domain to the set of real numbers. Journal of Formalized Mathematics, 5, 1993.

[16] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.

[17] Andrzej Trybulec. Subsets of real numbers. Journal of Formalized Mathematics, Addenda, 2003.

[18] Andrzej Trybulec and Czeslaw Bylinski. Some properties of real numbers operations: min, max, square, and square root. Journal of Formalized Mathematics, 1, 1989.

[19] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.

[20] Edmund Woronowicz. Relations and their basic properties. Journal of Formalized Mathematics, 1, 1989.

[21] Edmund Woronowicz. Relations defined on sets. Journal of Formalized Mathematics, 1, 1989.