Abian's Fixed Point Theorem

Piotr Rudnicki

University of Alberta, Edmonton

Andrzej Trybulec

Warsaw University, Bialystok

Summary.

A. Abian [1] proved the following theorem: \begin{quotation} Let $f$ be a mapping from a finite set $D$. Then $f$ has a fixed point if and only if $D$ is not a union of three mutually disjoint sets $A$, $B$ and $C$ such that \[ A \cap f[A] = B \cap f[B] = C \cap f[C] = \emptyset.\] \end{quotation} (The range of $f$ is not necessarily the subset of its domain). The proof of the sufficiency is by induction on the number of elements of $D$. A.~M\c{a}kowski and K.~Wi{\'s}niewski [10] have shown that the assumption of finiteness is superfluous. They proved their version of the theorem for $f$ being a function from $D$ into $D$. In the proof, the required partition was constructed and the construction used the axiom of choice. Their main point was to demonstrate that the use of this axiom in the proof is essential. We have proved in Mizar the generalized version of Abian's theorem, i.e. without assuming finiteness of $D$. We have simplified the proof from [10] which uses well-ordering principle and transfinite ordinals-our proof does not use these notions but otherwise is based on their idea (we employ choice functions).

This work was partially supported by NSERC Grant OGP9207 and NATO CRG 951368.

MML Identifier: ABIAN

Contents (PDF format)

Bibliography

[1] A. Abian. A fixed point theorem. \em Nieuw Arch. Wisk., 3(16):184--185, 1968.

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

[3] Grzegorz Bancerek. The ordinal numbers. Journal of Formalized Mathematics, 1, 1989.

[4] Grzegorz Bancerek and Andrzej Trybulec. Miscellaneous facts about functions. Journal of Formalized Mathematics, 8, 1996.

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

[6] Czeslaw Bylinski. Functions from a set to a set. Journal of Formalized Mathematics, 1, 1989.

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

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

[9] Agata Darmochwal and Andrzej Trybulec. Similarity of formulae. Journal of Formalized Mathematics, 3, 1991.

[10] A. Makowski and K. Wisniewski. Generalization of Abian's fixed point theorem. \em Annales Soc. Math. Pol. Series I, XIII:63--65, 1969.

[11] Beata Padlewska. Families of sets. Journal of Formalized Mathematics, 1, 1989.

[12] Konrad Raczkowski and Pawel Sadowski. Equivalence relations and classes of abstraction. Journal of Formalized Mathematics, 1, 1989.

[13] Piotr Rudnicki and Andrzej Trybulec. Fixpoints in complete lattices. Journal of Formalized Mathematics, 8, 1996.

[14] Andrzej Trybulec. Binary operations applied to functions. Journal of Formalized Mathematics, 1, 1989.

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

[16] Andrzej Trybulec. Tuples, projections and Cartesian products. Journal of Formalized Mathematics, 1, 1989.

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

[18] Michal J. Trybulec. Integers. Journal of Formalized Mathematics, 2, 1990.

[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.