Journal of Formalized Mathematics
Volume 15, 2003
University of Bialystok
Copyright (c) 2003 Association of Mizar Users

On the Sets Inhabited by Numbers


Andrzej Trybulec
University of Bialystok

Summary.

The information that all members of a set enjoy a property expressed by an adjective can be processed in a systematic way. The purpose of the work is to find out how to do that. If it works, `membered' will become a reserved word and the work with it will be automated. I have chosen {\it membered} rather than {\it inhabited} because of the compatibility with the Automath terminology. The phrase $\tau$ {\it inhabits} $\theta$ could be translated to $\tau$ {\bfseries\itshape is} $\theta$ in Mizar.

This work has been partially supported by the CALCULEMUS grant HPRN-CT-2000-00102.

MML Identifier: MEMBERED

The terminology and notation used in this paper have been introduced in the following articles [5] [8] [4] [6] [3] [7] [1] [2]

Contents (PDF format)

Acknowledgments

I am grateful to Dr. Czeslaw Bylinski for the discussion, particularly for his advice to prove more trivial but useful theorems.

Bibliography

[1] Grzegorz Bancerek. The ordinal numbers. Journal of Formalized Mathematics, 1, 1989.
[2] Grzegorz Bancerek. Sequences of ordinal numbers. Journal of Formalized Mathematics, 1, 1989.
[3] Andrzej Kondracki. Basic properties of rational numbers. Journal of Formalized Mathematics, 2, 1990.
[4] Beata Padlewska. Families of sets. Journal of Formalized Mathematics, 1, 1989.
[5] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.
[6] Andrzej Trybulec. Subsets of real numbers. Journal of Formalized Mathematics, Addenda, 2003.
[7] Michal J. Trybulec. Integers. Journal of Formalized Mathematics, 2, 1990.
[8] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.

Received August 23, 2003


[ Download a postscript version, MML identifier index, Mizar home page]